:: RECDEF_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let x be set ;
given x1, x2, x3 being set such that A1: x = [x1,x2,x3] ;
func x `1_3 -> set means :Def1: :: RECDEF_2:def 1
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y1;
existence
ex b1 being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y1 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y1 ) holds
b1 = b2
proof end;
func x `2_3 -> set means :Def2: :: RECDEF_2:def 2
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y2;
existence
ex b1 being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y2 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y2 ) holds
b1 = b2
proof end;
func x `3_3 -> set means :Def3: :: RECDEF_2:def 3
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y3;
existence
ex b1 being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y3
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y3 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines `1_3 RECDEF_2:def 1 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b2 being set holds
( b2 = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y1 );

:: deftheorem Def2 defines `2_3 RECDEF_2:def 2 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b2 being set holds
( b2 = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y2 );

:: deftheorem Def3 defines `3_3 RECDEF_2:def 3 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b2 being set holds
( b2 = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y3 );

theorem Th1: :: RECDEF_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being set st ex a, b, c being set st z = [a,b,c] holds
z = [(z `1_3 ),(z `2_3 ),(z `3_3 )]
proof end;

theorem :: RECDEF_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C being set st z in [:A,B,C:] holds
( z `1_3 in A & z `2_3 in B & z `3_3 in C )
proof end;

theorem :: RECDEF_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C being set st z in [:A,B,C:] holds
z = [(z `1_3 ),(z `2_3 ),(z `3_3 )]
proof end;

definition
let x be set ;
given x1, x2, x3, x4 being set such that A1: x = [x1,x2,x3,x4] ;
func x `1_4 -> set means :Def4: :: RECDEF_2:def 4
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y1;
existence
ex b1 being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y1 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y1 ) holds
b1 = b2
proof end;
func x `2_4 -> set means :Def5: :: RECDEF_2:def 5
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y2;
existence
ex b1 being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y2 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y2 ) holds
b1 = b2
proof end;
func x `3_4 -> set means :Def6: :: RECDEF_2:def 6
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y3;
existence
ex b1 being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y3
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y3 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y3 ) holds
b1 = b2
proof end;
func x `4_4 -> set means :Def7: :: RECDEF_2:def 7
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y4;
existence
ex b1 being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y4
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y4 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines `1_4 RECDEF_2:def 4 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b2 being set holds
( b2 = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y1 );

:: deftheorem Def5 defines `2_4 RECDEF_2:def 5 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b2 being set holds
( b2 = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y2 );

:: deftheorem Def6 defines `3_4 RECDEF_2:def 6 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b2 being set holds
( b2 = x `3_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y3 );

:: deftheorem Def7 defines `4_4 RECDEF_2:def 7 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b2 being set holds
( b2 = x `4_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y4 );

theorem Th4: :: RECDEF_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being set st ex a, b, c, d being set st z = [a,b,c,d] holds
z = [(z `1_4 ),(z `2_4 ),(z `3_4 ),(z `4_4 )]
proof end;

theorem :: RECDEF_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C, D being set st z in [:A,B,C,D:] holds
( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )
proof end;

theorem :: RECDEF_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C, D being set st z in [:A,B,C,D:] holds
z = [(z `1_4 ),(z `2_4 ),(z `3_4 ),(z `4_4 )]
proof end;

definition
let x be set ;
given x1, x2, x3, x4, x5 being set such that A1: x = [x1,x2,x3,x4,x5] ;
func x `1_5 -> set means :Def8: :: RECDEF_2:def 8
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y1;
existence
ex b1 being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y1 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y1 ) holds
b1 = b2
proof end;
func x `2_5 -> set means :Def9: :: RECDEF_2:def 9
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y2;
existence
ex b1 being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y2 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y2 ) holds
b1 = b2
proof end;
func x `3_5 -> set means :Def10: :: RECDEF_2:def 10
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y3;
existence
ex b1 being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y3
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y3 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y3 ) holds
b1 = b2
proof end;
func x `4_5 -> set means :Def11: :: RECDEF_2:def 11
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y4;
existence
ex b1 being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y4
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y4 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y4 ) holds
b1 = b2
proof end;
func x `5_5 -> set means :Def12: :: RECDEF_2:def 12
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y5;
existence
ex b1 being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y5
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b1 = y5 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `1_5 RECDEF_2:def 8 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b2 being set holds
( b2 = x `1_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y1 );

:: deftheorem Def9 defines `2_5 RECDEF_2:def 9 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b2 being set holds
( b2 = x `2_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y2 );

:: deftheorem Def10 defines `3_5 RECDEF_2:def 10 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b2 being set holds
( b2 = x `3_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y3 );

:: deftheorem Def11 defines `4_5 RECDEF_2:def 11 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b2 being set holds
( b2 = x `4_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y4 );

:: deftheorem Def12 defines `5_5 RECDEF_2:def 12 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b2 being set holds
( b2 = x `5_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b2 = y5 );

theorem Th7: :: RECDEF_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being set st ex a, b, c, d, e being set st z = [a,b,c,d,e] holds
z = [(z `1_5 ),(z `2_5 ),(z `3_5 ),(z `4_5 ),(z `5_5 )]
proof end;

theorem :: RECDEF_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C, D, E being set st z in [:A,B,C,D,E:] holds
( z `1_5 in A & z `2_5 in B & z `3_5 in C & z `4_5 in D & z `5_5 in E )
proof end;

theorem :: RECDEF_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, A, B, C, D, E being set st z in [:A,B,C,D,E:] holds
z = [(z `1_5 ),(z `2_5 ),(z `3_5 ),(z `4_5 ),(z `5_5 )]
proof end;

scheme :: RECDEF_2:sch 1
ExFunc3Cond{ F1() -> set , P1[ set ], P2[ set ], P3[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ) )
provided
A1: for c being set st c in F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) and
A2: for c being set holds
( not c in F1() or P1[c] or P2[c] or P3[c] )
proof end;

scheme :: RECDEF_2:sch 2
ExFunc4Cond{ F1() -> set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set , F5( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) & ( P4[c] implies f . c = F5(c) ) ) ) )
provided
A1: for c being set st c in F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) and
A2: for c being set holds
( not c in F1() or P1[c] or P2[c] or P3[c] or P4[c] )
proof end;

scheme :: RECDEF_2:sch 3
DoubleChoiceRec{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F2(), P1[ set , set , set , set , set ] } :
ex f being Function of NAT ,F1() ex g being Function of NAT ,F2() st
( f . 0 = F3() & g . 0 = F4() & ( for n being Element of NAT holds P1[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being Element of F1()
for y being Element of F2() ex x1 being Element of F1() ex y1 being Element of F2() st P1[n,x,y,x1,y1]
proof end;

scheme :: RECDEF_2:sch 4
LambdaRec2Ex{ F1() -> set , F2() -> set , F3( set , set , set ) -> set } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & ( for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
proof end;

scheme :: RECDEF_2:sch 5
LambdaRec2ExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1() } :
ex f being Function of NAT ,F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) )
proof end;

scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F1() -> set , F2() -> set , F3() -> Function, F4() -> Function, F5( set , set , set ) -> set } :
F3() = F4()
provided
A1: dom F3() = NAT and
A2: ( F3() . 0 = F1() & F3() . 1 = F2() ) and
A3: for n being Nat holds F3() . (n + 2) = F5(n,(F3() . n),(F3() . (n + 1))) and
A4: dom F4() = NAT and
A5: ( F4() . 0 = F1() & F4() . 1 = F2() ) and
A6: for n being Nat holds F4() . (n + 2) = F5(n,(F4() . n),(F4() . (n + 1)))
proof end;

scheme :: RECDEF_2:sch 7
LambdaRec2UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Function of NAT ,F1(), F5() -> Function of NAT ,F1(), F6( set , set , set ) -> Element of F1() } :
F4() = F5()
provided
A1: ( F4() . 0 = F2() & F4() . 1 = F3() ) and
A2: for n being Nat holds F4() . (n + 2) = F6(n,(F4() . n),(F4() . (n + 1))) and
A3: ( F5() . 0 = F2() & F5() . 1 = F3() ) and
A4: for n being Nat holds F5() . (n + 2) = F6(n,(F5() . n),(F5() . (n + 1)))
proof end;

scheme :: RECDEF_2:sch 8
LambdaRec3Ex{ F1() -> set , F2() -> set , F3() -> set , F4( set , set , set , set ) -> set } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & ( for n being Nat holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof end;

scheme :: RECDEF_2:sch 9
LambdaRec3ExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5( set , set , set , set ) -> Element of F1() } :
ex f being Function of NAT ,F1() st
( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() & ( for n being Nat holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof end;

scheme :: RECDEF_2:sch 10
LambdaRec3Un{ F1() -> set , F2() -> set , F3() -> set , F4() -> Function, F5() -> Function, F6( set , set , set , set ) -> set } :
F4() = F5()
provided
A1: dom F4() = NAT and
A2: ( F4() . 0 = F1() & F4() . 1 = F2() & F4() . 2 = F3() ) and
A3: for n being Nat holds F4() . (n + 3) = F6(n,(F4() . n),(F4() . (n + 1)),(F4() . (n + 2))) and
A4: dom F5() = NAT and
A5: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() ) and
A6: for n being Nat holds F5() . (n + 3) = F6(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2)))
proof end;

scheme :: RECDEF_2:sch 11
LambdaRec3UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Function of NAT ,F1(), F6() -> Function of NAT ,F1(), F7( set , set , set , set ) -> Element of F1() } :
F5() = F6()
provided
A1: ( F5() . 0 = F2() & F5() . 1 = F3() & F5() . 2 = F4() ) and
A2: for n being Nat holds F5() . (n + 3) = F7(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2))) and
A3: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() ) and
A4: for n being Nat holds F6() . (n + 3) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)))
proof end;

scheme :: RECDEF_2:sch 12
LambdaRec4Ex{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5( set , set , set , set , set ) -> set } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & f . 3 = F4() & ( for n being Nat holds f . (n + 4) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
proof end;

scheme :: RECDEF_2:sch 13
LambdaRec4ExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F1(), F6( set , set , set , set , set ) -> Element of F1() } :
ex f being Function of NAT ,F1() st
( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() & f . 3 = F5() & ( for n being Nat holds f . (n + 4) = F6(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
proof end;

scheme :: RECDEF_2:sch 14
LambdaRec4Un{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5() -> Function, F6() -> Function, F7( set , set , set , set , set ) -> set } :
F5() = F6()
provided
A1: dom F5() = NAT and
A2: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() & F5() . 3 = F4() ) and
A3: for n being Nat holds F5() . (n + 4) = F7(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2)),(F5() . (n + 3))) and
A4: dom F6() = NAT and
A5: ( F6() . 0 = F1() & F6() . 1 = F2() & F6() . 2 = F3() & F6() . 3 = F4() ) and
A6: for n being Nat holds F6() . (n + 4) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)),(F6() . (n + 3)))
proof end;

scheme :: RECDEF_2:sch 15
LambdaRec4UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Function of NAT ,F1(), F7() -> Function of NAT ,F1(), F8( set , set , set , set , set ) -> Element of F1() } :
F6() = F7()
provided
A1: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() & F6() . 3 = F5() ) and
A2: for n being Nat holds F6() . (n + 4) = F8(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)),(F6() . (n + 3))) and
A3: ( F7() . 0 = F2() & F7() . 1 = F3() & F7() . 2 = F4() & F7() . 3 = F5() ) and
A4: for n being Nat holds F7() . (n + 4) = F8(n,(F7() . n),(F7() . (n + 1)),(F7() . (n + 2)),(F7() . (n + 3)))
proof end;