:: RECDEF_2 semantic presentation

definition
let c1 be set ;
given c2, c3, c4 being set such that E1: c1 = [c2,c3,c4] ;
func c1 `1_3 -> set means :Def1: :: RECDEF_2:def 1
for b1, b2, b3 being set st a1 = [b1,b2,b3] holds
a2 = b1;
existence
ex b1 being set st
for b2, b3, b4 being set st c1 = [b2,b3,b4] holds
b1 = b2
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b1 = b3 ) & ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b2 = b3 ) holds
b1 = b2
proof end;
func c1 `2_3 -> set means :Def2: :: RECDEF_2:def 2
for b1, b2, b3 being set st a1 = [b1,b2,b3] holds
a2 = b2;
existence
ex b1 being set st
for b2, b3, b4 being set st c1 = [b2,b3,b4] holds
b1 = b3
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b1 = b4 ) & ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b2 = b4 ) holds
b1 = b2
proof end;
func c1 `3_3 -> set means :Def3: :: RECDEF_2:def 3
for b1, b2, b3 being set st a1 = [b1,b2,b3] holds
a2 = b3;
existence
ex b1 being set st
for b2, b3, b4 being set st c1 = [b2,b3,b4] holds
b1 = b4
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b1 = b5 ) & ( for b3, b4, b5 being set st c1 = [b3,b4,b5] holds
b2 = b5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines `1_3 RECDEF_2:def 1 :
for b1 being set st ex b2, b3, b4 being set st b1 = [b2,b3,b4] holds
for b2 being set holds
( b2 = b1 `1_3 iff for b3, b4, b5 being set st b1 = [b3,b4,b5] holds
b2 = b3 );

:: deftheorem Def2 defines `2_3 RECDEF_2:def 2 :
for b1 being set st ex b2, b3, b4 being set st b1 = [b2,b3,b4] holds
for b2 being set holds
( b2 = b1 `2_3 iff for b3, b4, b5 being set st b1 = [b3,b4,b5] holds
b2 = b4 );

:: deftheorem Def3 defines `3_3 RECDEF_2:def 3 :
for b1 being set st ex b2, b3, b4 being set st b1 = [b2,b3,b4] holds
for b2 being set holds
( b2 = b1 `3_3 iff for b3, b4, b5 being set st b1 = [b3,b4,b5] holds
b2 = b5 );

theorem Th1: :: RECDEF_2:1
for b1 being set st ex b2, b3, b4 being set st b1 = [b2,b3,b4] holds
b1 = [(b1 `1_3 ),(b1 `2_3 ),(b1 `3_3 )]
proof end;

theorem Th2: :: RECDEF_2:2
for b1, b2, b3, b4 being set st b1 in [:b2,b3,b4:] holds
( b1 `1_3 in b2 & b1 `2_3 in b3 & b1 `3_3 in b4 )
proof end;

theorem Th3: :: RECDEF_2:3
for b1, b2, b3, b4 being set st b1 in [:b2,b3,b4:] holds
b1 = [(b1 `1_3 ),(b1 `2_3 ),(b1 `3_3 )]
proof end;

definition
let c1 be set ;
given c2, c3, c4, c5 being set such that E5: c1 = [c2,c3,c4,c5] ;
func c1 `1_4 -> set means :Def4: :: RECDEF_2:def 4
for b1, b2, b3, b4 being set st a1 = [b1,b2,b3,b4] holds
a2 = b1;
existence
ex b1 being set st
for b2, b3, b4, b5 being set st c1 = [b2,b3,b4,b5] holds
b1 = b2
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b1 = b3 ) & ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b2 = b3 ) holds
b1 = b2
proof end;
func c1 `2_4 -> set means :Def5: :: RECDEF_2:def 5
for b1, b2, b3, b4 being set st a1 = [b1,b2,b3,b4] holds
a2 = b2;
existence
ex b1 being set st
for b2, b3, b4, b5 being set st c1 = [b2,b3,b4,b5] holds
b1 = b3
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b1 = b4 ) & ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b2 = b4 ) holds
b1 = b2
proof end;
func c1 `3_4 -> set means :Def6: :: RECDEF_2:def 6
for b1, b2, b3, b4 being set st a1 = [b1,b2,b3,b4] holds
a2 = b3;
existence
ex b1 being set st
for b2, b3, b4, b5 being set st c1 = [b2,b3,b4,b5] holds
b1 = b4
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b1 = b5 ) & ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b2 = b5 ) holds
b1 = b2
proof end;
func c1 `4_4 -> set means :Def7: :: RECDEF_2:def 7
for b1, b2, b3, b4 being set st a1 = [b1,b2,b3,b4] holds
a2 = b4;
existence
ex b1 being set st
for b2, b3, b4, b5 being set st c1 = [b2,b3,b4,b5] holds
b1 = b5
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b1 = b6 ) & ( for b3, b4, b5, b6 being set st c1 = [b3,b4,b5,b6] holds
b2 = b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines `1_4 RECDEF_2:def 4 :
for b1 being set st ex b2, b3, b4, b5 being set st b1 = [b2,b3,b4,b5] holds
for b2 being set holds
( b2 = b1 `1_4 iff for b3, b4, b5, b6 being set st b1 = [b3,b4,b5,b6] holds
b2 = b3 );

:: deftheorem Def5 defines `2_4 RECDEF_2:def 5 :
for b1 being set st ex b2, b3, b4, b5 being set st b1 = [b2,b3,b4,b5] holds
for b2 being set holds
( b2 = b1 `2_4 iff for b3, b4, b5, b6 being set st b1 = [b3,b4,b5,b6] holds
b2 = b4 );

:: deftheorem Def6 defines `3_4 RECDEF_2:def 6 :
for b1 being set st ex b2, b3, b4, b5 being set st b1 = [b2,b3,b4,b5] holds
for b2 being set holds
( b2 = b1 `3_4 iff for b3, b4, b5, b6 being set st b1 = [b3,b4,b5,b6] holds
b2 = b5 );

:: deftheorem Def7 defines `4_4 RECDEF_2:def 7 :
for b1 being set st ex b2, b3, b4, b5 being set st b1 = [b2,b3,b4,b5] holds
for b2 being set holds
( b2 = b1 `4_4 iff for b3, b4, b5, b6 being set st b1 = [b3,b4,b5,b6] holds
b2 = b6 );

theorem Th4: :: RECDEF_2:4
for b1 being set st ex b2, b3, b4, b5 being set st b1 = [b2,b3,b4,b5] holds
b1 = [(b1 `1_4 ),(b1 `2_4 ),(b1 `3_4 ),(b1 `4_4 )]
proof end;

theorem Th5: :: RECDEF_2:5
for b1, b2, b3, b4, b5 being set st b1 in [:b2,b3,b4,b5:] holds
( b1 `1_4 in b2 & b1 `2_4 in b3 & b1 `3_4 in b4 & b1 `4_4 in b5 )
proof end;

theorem Th6: :: RECDEF_2:6
for b1, b2, b3, b4, b5 being set st b1 in [:b2,b3,b4,b5:] holds
b1 = [(b1 `1_4 ),(b1 `2_4 ),(b1 `3_4 ),(b1 `4_4 )]
proof end;

definition
let c1 be set ;
given c2, c3, c4, c5, c6 being set such that E10: c1 = [c2,c3,c4,c5,c6] ;
func c1 `1_5 -> set means :Def8: :: RECDEF_2:def 8
for b1, b2, b3, b4, b5 being set st a1 = [b1,b2,b3,b4,b5] holds
a2 = b1;
existence
ex b1 being set st
for b2, b3, b4, b5, b6 being set st c1 = [b2,b3,b4,b5,b6] holds
b1 = b2
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b1 = b3 ) & ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b2 = b3 ) holds
b1 = b2
proof end;
func c1 `2_5 -> set means :Def9: :: RECDEF_2:def 9
for b1, b2, b3, b4, b5 being set st a1 = [b1,b2,b3,b4,b5] holds
a2 = b2;
existence
ex b1 being set st
for b2, b3, b4, b5, b6 being set st c1 = [b2,b3,b4,b5,b6] holds
b1 = b3
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b1 = b4 ) & ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b2 = b4 ) holds
b1 = b2
proof end;
func c1 `3_5 -> set means :Def10: :: RECDEF_2:def 10
for b1, b2, b3, b4, b5 being set st a1 = [b1,b2,b3,b4,b5] holds
a2 = b3;
existence
ex b1 being set st
for b2, b3, b4, b5, b6 being set st c1 = [b2,b3,b4,b5,b6] holds
b1 = b4
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b1 = b5 ) & ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b2 = b5 ) holds
b1 = b2
proof end;
func c1 `4_5 -> set means :Def11: :: RECDEF_2:def 11
for b1, b2, b3, b4, b5 being set st a1 = [b1,b2,b3,b4,b5] holds
a2 = b4;
existence
ex b1 being set st
for b2, b3, b4, b5, b6 being set st c1 = [b2,b3,b4,b5,b6] holds
b1 = b5
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b1 = b6 ) & ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b2 = b6 ) holds
b1 = b2
proof end;
func c1 `5_5 -> set means :Def12: :: RECDEF_2:def 12
for b1, b2, b3, b4, b5 being set st a1 = [b1,b2,b3,b4,b5] holds
a2 = b5;
existence
ex b1 being set st
for b2, b3, b4, b5, b6 being set st c1 = [b2,b3,b4,b5,b6] holds
b1 = b6
proof end;
uniqueness
for b1, b2 being set st ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b1 = b7 ) & ( for b3, b4, b5, b6, b7 being set st c1 = [b3,b4,b5,b6,b7] holds
b2 = b7 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `1_5 RECDEF_2:def 8 :
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
for b2 being set holds
( b2 = b1 `1_5 iff for b3, b4, b5, b6, b7 being set st b1 = [b3,b4,b5,b6,b7] holds
b2 = b3 );

:: deftheorem Def9 defines `2_5 RECDEF_2:def 9 :
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
for b2 being set holds
( b2 = b1 `2_5 iff for b3, b4, b5, b6, b7 being set st b1 = [b3,b4,b5,b6,b7] holds
b2 = b4 );

:: deftheorem Def10 defines `3_5 RECDEF_2:def 10 :
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
for b2 being set holds
( b2 = b1 `3_5 iff for b3, b4, b5, b6, b7 being set st b1 = [b3,b4,b5,b6,b7] holds
b2 = b5 );

:: deftheorem Def11 defines `4_5 RECDEF_2:def 11 :
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
for b2 being set holds
( b2 = b1 `4_5 iff for b3, b4, b5, b6, b7 being set st b1 = [b3,b4,b5,b6,b7] holds
b2 = b6 );

:: deftheorem Def12 defines `5_5 RECDEF_2:def 12 :
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
for b2 being set holds
( b2 = b1 `5_5 iff for b3, b4, b5, b6, b7 being set st b1 = [b3,b4,b5,b6,b7] holds
b2 = b7 );

theorem Th7: :: RECDEF_2:7
for b1 being set st ex b2, b3, b4, b5, b6 being set st b1 = [b2,b3,b4,b5,b6] holds
b1 = [(b1 `1_5 ),(b1 `2_5 ),(b1 `3_5 ),(b1 `4_5 ),(b1 `5_5 )]
proof end;

theorem Th8: :: RECDEF_2:8
for b1, b2, b3, b4, b5, b6 being set st b1 in [:b2,b3,b4,b5,b6:] holds
( b1 `1_5 in b2 & b1 `2_5 in b3 & b1 `3_5 in b4 & b1 `4_5 in b5 & b1 `5_5 in b6 )
proof end;

theorem Th9: :: RECDEF_2:9
for b1, b2, b3, b4, b5, b6 being set st b1 in [:b2,b3,b4,b5,b6:] holds
b1 = [(b1 `1_5 ),(b1 `2_5 ),(b1 `3_5 ),(b1 `4_5 ),(b1 `5_5 )]
proof end;

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

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

scheme :: RECDEF_2:sch 3
s3{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F2(), P1[ set , set , set , set , set ] } :
ex b1 being Function of NAT ,F1()ex b2 being Function of NAT ,F2() st
( b1 . 0 = F3() & b2 . 0 = F4() & ( for b3 being Element of NAT holds P1[b3,b1 . b3,b2 . b3,b1 . (b3 + 1),b2 . (b3 + 1)] ) )
provided
E16: for b1 being Element of NAT
for b2 being Element of F1()
for b3 being Element of F2() ex b4 being Element of F1()ex b5 being Element of F2() st P1[b1,b2,b3,b4,b5]
proof end;

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

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

scheme :: RECDEF_2:sch 6
s6{ F1() -> set , F2() -> set , F3() -> Function, F4() -> Function, F5( set , set , set ) -> set } :
F3() = F4()
provided
E16: dom F3() = NAT and
E17: ( F3() . 0 = F1() & F3() . 1 = F2() ) and
E18: for b1 being Nat holds F3() . (b1 + 2) = F5(b1,(F3() . b1),(F3() . (b1 + 1))) and
E19: dom F4() = NAT and
E20: ( F4() . 0 = F1() & F4() . 1 = F2() ) and
E21: for b1 being Nat holds F4() . (b1 + 2) = F5(b1,(F4() . b1),(F4() . (b1 + 1)))
proof end;

scheme :: RECDEF_2:sch 7
s7{ 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
E16: ( F4() . 0 = F2() & F4() . 1 = F3() ) and
E17: for b1 being Nat holds F4() . (b1 + 2) = F6(b1,(F4() . b1),(F4() . (b1 + 1))) and
E18: ( F5() . 0 = F2() & F5() . 1 = F3() ) and
E19: for b1 being Nat holds F5() . (b1 + 2) = F6(b1,(F5() . b1),(F5() . (b1 + 1)))
proof end;

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

scheme :: RECDEF_2:sch 9
s9{ 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 b1 being Function of NAT ,F1() st
( b1 . 0 = F2() & b1 . 1 = F3() & b1 . 2 = F4() & ( for b2 being Nat holds b1 . (b2 + 3) = F5(b2,(b1 . b2),(b1 . (b2 + 1)),(b1 . (b2 + 2))) ) )
proof end;

scheme :: RECDEF_2:sch 10
s10{ F1() -> set , F2() -> set , F3() -> set , F4() -> Function, F5() -> Function, F6( set , set , set , set ) -> set } :
F4() = F5()
provided
E16: dom F4() = NAT and
E17: ( F4() . 0 = F1() & F4() . 1 = F2() & F4() . 2 = F3() ) and
E18: for b1 being Nat holds F4() . (b1 + 3) = F6(b1,(F4() . b1),(F4() . (b1 + 1)),(F4() . (b1 + 2))) and
E19: dom F5() = NAT and
E20: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() ) and
E21: for b1 being Nat holds F5() . (b1 + 3) = F6(b1,(F5() . b1),(F5() . (b1 + 1)),(F5() . (b1 + 2)))
proof end;

scheme :: RECDEF_2:sch 11
s11{ 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
E16: ( F5() . 0 = F2() & F5() . 1 = F3() & F5() . 2 = F4() ) and
E17: for b1 being Nat holds F5() . (b1 + 3) = F7(b1,(F5() . b1),(F5() . (b1 + 1)),(F5() . (b1 + 2))) and
E18: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() ) and
E19: for b1 being Nat holds F6() . (b1 + 3) = F7(b1,(F6() . b1),(F6() . (b1 + 1)),(F6() . (b1 + 2)))
proof end;

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

scheme :: RECDEF_2:sch 13
s13{ 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 b1 being Function of NAT ,F1() st
( b1 . 0 = F2() & b1 . 1 = F3() & b1 . 2 = F4() & b1 . 3 = F5() & ( for b2 being Nat holds b1 . (b2 + 4) = F6(b2,(b1 . b2),(b1 . (b2 + 1)),(b1 . (b2 + 2)),(b1 . (b2 + 3))) ) )
proof end;

scheme :: RECDEF_2:sch 14
s14{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5() -> Function, F6() -> Function, F7( set , set , set , set , set ) -> set } :
F5() = F6()
provided
E16: dom F5() = NAT and
E17: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() & F5() . 3 = F4() ) and
E18: for b1 being Nat holds F5() . (b1 + 4) = F7(b1,(F5() . b1),(F5() . (b1 + 1)),(F5() . (b1 + 2)),(F5() . (b1 + 3))) and
E19: dom F6() = NAT and
E20: ( F6() . 0 = F1() & F6() . 1 = F2() & F6() . 2 = F3() & F6() . 3 = F4() ) and
E21: for b1 being Nat holds F6() . (b1 + 4) = F7(b1,(F6() . b1),(F6() . (b1 + 1)),(F6() . (b1 + 2)),(F6() . (b1 + 3)))
proof end;

scheme :: RECDEF_2:sch 15
s15{ 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
E16: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() & F6() . 3 = F5() ) and
E17: for b1 being Nat holds F6() . (b1 + 4) = F8(b1,(F6() . b1),(F6() . (b1 + 1)),(F6() . (b1 + 2)),(F6() . (b1 + 3))) and
E18: ( F7() . 0 = F2() & F7() . 1 = F3() & F7() . 2 = F4() & F7() . 3 = F5() ) and
E19: for b1 being Nat holds F7() . (b1 + 4) = F8(b1,(F7() . b1),(F7() . (b1 + 1)),(F7() . (b1 + 2)),(F7() . (b1 + 3)))
proof end;