:: RECDEF_2 semantic presentation

begin


definition
let x be triple set ;
consider x1, x2, x3 being set  such that
A1: x = [x1,x2,x3] by XTUPLE_0:def_5;
A2: [x1,x2,x3] `1_3 = x1 ;
A3: [x1,x2,x3] `2_3 = x2 ;
A4: [x1,x2,x3] `3_3 = x3 ;
redefine func x `1_3  means :Def1: :: RECDEF_2:def 1
 for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y1;
compatibility
 for b1 being set holds
( b1 = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y1 ) by A1, A2, XTUPLE_0:3;
redefine func x `2_3  means :Def2: :: RECDEF_2:def 2
 for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y2;
compatibility
 for b1 being set holds
( b1 = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y2 ) by A1, A3, XTUPLE_0:3;
redefine func x `2  means :Def3: :: RECDEF_2:def 3
 for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y3;
compatibility
 for b1 being set holds
( b1 = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y3 ) by A1, A4, XTUPLE_0:3;
end;

:: deftheorem Def1 defines `1_3 RECDEF_2:def_1_:_
 for x being triple set
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 triple set
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 triple set
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
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
let z be set ; ::_thesis: ( ex a, b, c being set st z = [a,b,c] implies z = [(z `1_3),(z `2_3),(z `3_3)] )
given a, b, c being set  such that A1: z = [a,b,c] ; ::_thesis: z = [(z `1_3),(z `2_3),(z `3_3)]
 ( z `1_3 = a & z `2_3 = b ) by A1, Def1, Def2;
hence  z = [(z `1_3),(z `2_3),(z `3_3)] by A1, Def3; ::_thesis: verum
end;

theorem :: RECDEF_2:2
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
let z, A, B, C be set ; ::_thesis: ( z in [:A,B,C:] implies ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) )
assume A1: z in [:A,B,C:] ; ::_thesis: ( z `1_3 in A & z `2_3 in B & z `3_3 in C )
then A2: not C is empty by MCART_1:31;
A3: ( not A is empty & not B is empty ) by A1, MCART_1:31;
then consider a being Element of A, b being Element of B, c being Element of C such that
A4: z = [a,b,c] by A1, A2, DOMAIN_1:3;
A5: z `3_3 = c by A4, Def3;
 ( z `1_3 = a & z `2_3 = b ) by A4, Def1, Def2;
hence  ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) by A3, A2, A5; ::_thesis: verum
end;

theorem Th3: :: RECDEF_2:3
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
let z, A, B, C be set ; ::_thesis: ( z in [:A,B,C:] implies z = [(z `1_3),(z `2_3),(z `3_3)] )
assume A1: z in [:A,B,C:] ; ::_thesis: z = [(z `1_3),(z `2_3),(z `3_3)]
then A2: not C is empty by MCART_1:31;
 ( not A is empty & not B is empty ) by A1, MCART_1:31;
then  ex a being Element of A ex b being Element of B ex c being Element of C st z = [a,b,c] by A1, A2, DOMAIN_1:3;
hence  z = [(z `1_3),(z `2_3),(z `3_3)] by Th1; ::_thesis: verum
end;

definition
let x be quadruple set ;
consider x1, x2, x3, x4 being set  such that
A1: x = [x1,x2,x3,x4] by XTUPLE_0:def_9;
A2: [x1,x2,x3,x4] `1_4 = x1 ;
A3: [x1,x2,x3,x4] `2_4 = x2 ;
A4: [x1,x2,x3,x4] `3_4 = x3 ;
A5: [x1,x2,x3,x4] `4_4 = x4 ;
redefine func x `1_4  means :Def4: :: RECDEF_2:def 4
 for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y1;
compatibility
 for b1 being set holds
( b1 = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y1 ) by A1, A2, XTUPLE_0:5;
redefine func x `2_4  means :Def5: :: RECDEF_2:def 5
 for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y2;
compatibility
 for b1 being set holds
( b1 = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y2 ) by A1, A3, XTUPLE_0:5;
redefine func x `2_3  means :Def6: :: RECDEF_2:def 6
 for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y3;
compatibility
 for b1 being set holds
( b1 = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y3 ) by A1, A4, XTUPLE_0:5;
redefine func x `2  means :Def7: :: RECDEF_2:def 7
 for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y4;
compatibility
 for b1 being set holds
( b1 = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y4 ) by A1, A5, XTUPLE_0:5;
end;

:: deftheorem Def4 defines `1_4 RECDEF_2:def_4_:_
 for x being quadruple set
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 quadruple set
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 `2_3 RECDEF_2:def_6_:_
 for x being quadruple set
for b2 being set holds
( b2 = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y3 );

:: deftheorem Def7 defines `3_3 RECDEF_2:def_7_:_
 for x being quadruple set
for b2 being set holds
( b2 = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y4 );

theorem Th4: :: RECDEF_2:4
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
let z be set ; ::_thesis: ( ex a, b, c, d being set st z = [a,b,c,d] implies z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] )
given a, b, c, d being set  such that A1: z = [a,b,c,d] ; ::_thesis: z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]
A2: z `3_4 = c by A1, Def6;
 ( z `1_4 = a & z `2_4 = b ) by A1, Def4, Def5;
hence  z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] by A1, A2, Def7; ::_thesis: verum
end;

theorem :: RECDEF_2:5
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
let z, A, B, C, D be set ; ::_thesis: ( z in [:A,B,C,D:] implies ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D ) )
assume A1: z in [:A,B,C,D:] ; ::_thesis: ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )
then A2: ( not C is empty & not D is empty ) by MCART_1:51;
A3: ( not A is empty & not B is empty ) by A1, MCART_1:51;
then consider a being Element of A, b being Element of B, c being Element of C, d being Element of D such that
A4: z = [a,b,c,d] by A1, A2, DOMAIN_1:10;
A5: ( z `3_4 = c & z `4_4 = d ) by A4, Def6, Def7;
 ( z `1_4 = a & z `2_4 = b ) by A4, Def4, Def5;
hence  ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D ) by A3, A2, A5; ::_thesis: verum
end;

theorem :: RECDEF_2:6
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
let z, A, B, C, D be set ; ::_thesis: ( z in [:A,B,C,D:] implies z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] )
assume A1: z in [:A,B,C,D:] ; ::_thesis: z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]
then A2: ( not C is empty & not D is empty ) by MCART_1:51;
 ( not A is empty & not B is empty ) by A1, MCART_1:51;
then  ex a being Element of A ex b being Element of B ex c being Element of C ex d being Element of D st z = [a,b,c,d] by A1, A2, DOMAIN_1:10;
hence  z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] by Th4; ::_thesis: verum
end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
end;

:: deftheorem  RECDEF_2:def_8_:_
canceled;

:: deftheorem  RECDEF_2:def_9_:_
canceled;

:: deftheorem  RECDEF_2:def_10_:_
canceled;

:: deftheorem  RECDEF_2:def_11_:_
canceled;

:: deftheorem  RECDEF_2:def_12_:_
canceled;

theorem :: RECDEF_2:7
canceled;

theorem :: RECDEF_2:8
canceled;

theorem :: RECDEF_2:9
canceled;

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
consider D1 being set  such that
A3: for x being set holds
( x in D1 iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
consider D3 being set  such that
A4: for x being set holds
( x in D3 iff ( x in F1() & P3[x] ) ) from XBOOLE_0:sch_1();
consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being set st x in D1 holds
f1 . x = F2(x) from FUNCT_1:sch_3();
consider D2 being set  such that
A7: for x being set holds
( x in D2 iff ( x in F1() & P2[x] ) ) from XBOOLE_0:sch_1();
consider f3 being Function such that
A8: dom f3 = D3 and
A9: for x being set st x in D3 holds
f3 . x = F4(x) from FUNCT_1:sch_3();
consider f2 being Function such that
A10: dom f2 = D2 and
A11: for x being set st x in D2 holds
f2 . x = F3(x) from FUNCT_1:sch_3();
set f = (f1 +* f2) +* f3;
take  (f1 +* f2) +* f3 ; ::_thesis: ( dom ((f1 +* f2) +* f3) = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies ((f1 +* f2) +* f3) . c = F2(c) ) & ( P2[c] implies ((f1 +* f2) +* f3) . c = F3(c) ) & ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) ) ) ) )
A12: dom ((f1 +* f2) +* f3) = (dom (f1 +* f2)) \/ (dom f3) by FUNCT_4:def_1
.= ((dom f1) \/ (dom f2)) \/ (dom f3) by FUNCT_4:def_1 ;
thus  dom ((f1 +* f2) +* f3) = F1() ::_thesis: for c being set st c in F1() holds
( ( P1[c] implies ((f1 +* f2) +* f3) . c = F2(c) ) & ( P2[c] implies ((f1 +* f2) +* f3) . c = F3(c) ) & ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) ) )
proof
A13: D3 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D3 or x in F1() )
thus  ( not x in D3 or x in F1() ) by A4; ::_thesis: verum
end;
A14: D2 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in F1() )
thus  ( not x in D2 or x in F1() ) by A7; ::_thesis: verum
end;
 D1 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in F1() )
thus  ( not x in D1 or x in F1() ) by A3; ::_thesis: verum
end;
then  D1 \/ D2 c= F1() by A14, XBOOLE_1:8;
hence  dom ((f1 +* f2) +* f3) c= F1() by A5, A10, A8, A12, A13, XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: F1() c= dom ((f1 +* f2) +* f3)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom ((f1 +* f2) +* f3) )
assume A15: x in F1() ; ::_thesis: x in dom ((f1 +* f2) +* f3)
then  ( P1[x] or P2[x] or P3[x] ) by A2;
then  ( x in D1 or x in D2 or x in D3 ) by A3, A7, A4, A15;
then  ( x in D1 \/ D2 or x in D3 ) by XBOOLE_0:def_3;
hence  x in dom ((f1 +* f2) +* f3) by A5, A10, A8, A12, XBOOLE_0:def_3; ::_thesis: verum
end;
let c be set ; ::_thesis: ( c in F1() implies ( ( P1[c] implies ((f1 +* f2) +* f3) . c = F2(c) ) & ( P2[c] implies ((f1 +* f2) +* f3) . c = F3(c) ) & ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) ) ) )
assume A16: c in F1() ; ::_thesis: ( ( P1[c] implies ((f1 +* f2) +* f3) . c = F2(c) ) & ( P2[c] implies ((f1 +* f2) +* f3) . c = F3(c) ) & ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) ) )
hereby  ::_thesis: ( ( P2[c] implies ((f1 +* f2) +* f3) . c = F3(c) ) & ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) ) )
assume A17: P1[c] ; ::_thesis: ((f1 +* f2) +* f3) . c = F2(c)
 P2[c] by A1, A16, A17;
then A19: not c in D2 by A7;
 P3[c] by A1, A16, A17;
then  not c in D3 by A4;
hence ((f1 +* f2) +* f3) . c = (f1 +* f2) . c by A8, FUNCT_4:11
.= f1 . c by A10, A19, FUNCT_4:11
.= F2(c) by A6, A17, A3, A16 ;
::_thesis: verum
end;
hereby  ::_thesis: ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) )
assume A20: P2[c] ; ::_thesis: ((f1 +* f2) +* f3) . c = F3(c)
 P3[c] by A1, A16, A20;
then  not c in D3 by A4;
hence ((f1 +* f2) +* f3) . c = (f1 +* f2) . c by A8, FUNCT_4:11
.= f2 . c by A10, A20, A7, A16, FUNCT_4:13
.= F3(c) by A11, A20, A7, A16 ;
::_thesis: verum
end;
assume Z: P3[c] ; ::_thesis: ((f1 +* f2) +* f3) . c = F4(c)
hence ((f1 +* f2) +* f3) . c = f3 . c by A8, A4, A16, FUNCT_4:13
.= F4(c) by A9, Z, A4, A16 ;
::_thesis: verum
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
consider D1 being set  such that
A3: for x being set holds
( x in D1 iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
consider D4 being set  such that
A4: for x being set holds
( x in D4 iff ( x in F1() & P4[x] ) ) from XBOOLE_0:sch_1();
consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being set st x in D1 holds
f1 . x = F2(x) from FUNCT_1:sch_3();
consider D2 being set  such that
A7: for x being set holds
( x in D2 iff ( x in F1() & P2[x] ) ) from XBOOLE_0:sch_1();
consider f2 being Function such that
A8: dom f2 = D2 and
A9: for x being set st x in D2 holds
f2 . x = F3(x) from FUNCT_1:sch_3();
consider D3 being set  such that
A10: for x being set holds
( x in D3 iff ( x in F1() & P3[x] ) ) from XBOOLE_0:sch_1();
consider f4 being Function such that
A11: dom f4 = D4 and
A12: for x being set st x in D4 holds
f4 . x = F5(x) from FUNCT_1:sch_3();
consider f3 being Function such that
A13: dom f3 = D3 and
A14: for x being set st x in D3 holds
f3 . x = F4(x) from FUNCT_1:sch_3();
set f = ((f1 +* f2) +* f3) +* f4;
take  ((f1 +* f2) +* f3) +* f4 ; ::_thesis: ( dom (((f1 +* f2) +* f3) +* f4) = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) ) ) )
A15: dom (((f1 +* f2) +* f3) +* f4) = (dom ((f1 +* f2) +* f3)) \/ (dom f4) by FUNCT_4:def_1
.= ((dom (f1 +* f2)) \/ (dom f3)) \/ (dom f4) by FUNCT_4:def_1
.= (((dom f1) \/ (dom f2)) \/ (dom f3)) \/ (dom f4) by FUNCT_4:def_1 ;
thus  dom (((f1 +* f2) +* f3) +* f4) = F1() ::_thesis: for c being set st c in F1() holds
( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
proof
A16: D4 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D4 or x in F1() )
thus  ( not x in D4 or x in F1() ) by A4; ::_thesis: verum
end;
A17: D3 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D3 or x in F1() )
thus  ( not x in D3 or x in F1() ) by A10; ::_thesis: verum
end;
A18: D2 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in F1() )
thus  ( not x in D2 or x in F1() ) by A7; ::_thesis: verum
end;
 D1 c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in F1() )
thus  ( not x in D1 or x in F1() ) by A3; ::_thesis: verum
end;
then  D1 \/ D2 c= F1() by A18, XBOOLE_1:8;
then  (D1 \/ D2) \/ D3 c= F1() by A17, XBOOLE_1:8;
hence  dom (((f1 +* f2) +* f3) +* f4) c= F1() by A5, A8, A13, A11, A15, A16, XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: F1() c= dom (((f1 +* f2) +* f3) +* f4)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom (((f1 +* f2) +* f3) +* f4) )
assume A19: x in F1() ; ::_thesis: x in dom (((f1 +* f2) +* f3) +* f4)
then  ( P1[x] or P2[x] or P3[x] or P4[x] ) by A2;
then  ( x in D1 or x in D2 or x in D3 or x in D4 ) by A3, A7, A10, A4, A19;
then  ( x in D1 \/ D2 or x in D3 or x in D4 ) by XBOOLE_0:def_3;
then  ( x in (D1 \/ D2) \/ D3 or x in D4 ) by XBOOLE_0:def_3;
hence  x in dom (((f1 +* f2) +* f3) +* f4) by A5, A8, A13, A11, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
let c be set ; ::_thesis: ( c in F1() implies ( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) ) )
assume A20: c in F1() ; ::_thesis: ( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
hereby  ::_thesis: ( ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
assume A21: P1[c] ; ::_thesis: (((f1 +* f2) +* f3) +* f4) . c = F2(c)
 P3[c] by A1, A20, A21;
then A23: not c in D3 by A10;
 P2[c] by A1, A20, A21;
then A24: not c in D2 by A7;
 P4[c] by A1, A20, A21;
then  not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= (f1 +* f2) . c by A13, A23, FUNCT_4:11
.= f1 . c by A8, A24, FUNCT_4:11
.= F2(c) by A6, A21, A3, A20 ;
::_thesis: verum
end;
hereby  ::_thesis: ( ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
assume A25: P2[c] ; ::_thesis: (((f1 +* f2) +* f3) +* f4) . c = F3(c)
 P3[c] by A1, A20, A25;
then A27: not c in D3 by A10;
 P4[c] by A1, A20, A25;
then  not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= (f1 +* f2) . c by A13, A27, FUNCT_4:11
.= f2 . c by A8, A25, A7, A20, FUNCT_4:13
.= F3(c) by A9, A25, A7, A20 ;
::_thesis: verum
end;
hereby  ::_thesis: ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) )
assume A28: P3[c] ; ::_thesis: (((f1 +* f2) +* f3) +* f4) . c = F4(c)
 P4[c] by A1, A20, A28;
then  not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= f3 . c by A13, A28, A10, A20, FUNCT_4:13
.= F4(c) by A14, A28, A10, A20 ;
::_thesis: verum
end;
assume Z: P4[c] ; ::_thesis: (((f1 +* f2) +* f3) +* f4) . c = F5(c)
hence (((f1 +* f2) +* f3) +* f4) . c = f4 . c by A11, A4, A20, FUNCT_4:13
.= F5(c) by A12, Z, A4, A20 ;
::_thesis: verum
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
defpred S1[ set , set , set ] means P1[$1,$2 `1 ,$2 `2 ,$3 `1 ,$3 `2 ];
A2: for n being Element of NAT
for x being Element of [:F1(),F2():] ex y being Element of [:F1(),F2():] st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of [:F1(),F2():] ex y being Element of [:F1(),F2():] st S1[n,x,y]
let x be Element of [:F1(),F2():]; ::_thesis: ex y being Element of [:F1(),F2():] st S1[n,x,y]
consider ai being Element of F1(), bi being Element of F2() such that
A3: P1[n,x `1 ,x `2 ,ai,bi] by A1;
take  [ai,bi] ; ::_thesis: S1[n,x,[ai,bi]]
thus  S1[n,x,[ai,bi]] by A3; ::_thesis: verum
end;
consider f being Function of NAT,[:F1(),F2():] such that
A4: f . 0 = [F3(),F4()] and
A5: for e being Element of NAT holds S1[e,f . e,f . (e + 1)] from RECDEF_1:sch_2(A2);
take  pr1 f ; ::_thesis: ex g being Function of NAT,F2() st
( (pr1 f) . 0 = F3() & g . 0 = F4() & ( for n being Element of NAT holds P1[n,(pr1 f) . n,g . n,(pr1 f) . (n + 1),g . (n + 1)] ) )
take  pr2 f ; ::_thesis: ( (pr1 f) . 0 = F3() & (pr2 f) . 0 = F4() & ( for n being Element of NAT holds P1[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)] ) )
 ( [F3(),F4()] `1 = F3() & [F3(),F4()] `2 = F4() ) ;
hence  ( (pr1 f) . 0 = F3() & (pr2 f) . 0 = F4() ) by A4, FUNCT_2:def_5, FUNCT_2:def_6; ::_thesis: for n being Element of NAT holds P1[n,(pr1 f) . n,(pr2 f) . n,(pr1 f) . (n + 1),(pr2 f) . (n + 1)]
let i be Element of NAT ; ::_thesis: P1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
A6: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def_5, FUNCT_2:def_6;
 ( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def_5, FUNCT_2:def_6;
hence  P1[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A5, A6; ::_thesis: verum
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 Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
proof
defpred S1[ set ] means $1 = 0 ;
deffunc H1( Nat, set ) ->  set = [($2 `2_3),($2 `3_3),F3(($1 + 1),($2 `2_3),($2 `3_3))];
set r03 = F3(0,F1(),F2());
set r13 = F3(1,F2(),F3(0,F1(),F2()));
deffunc H2( Nat, set ) ->  set = H1($1 + 1,$2);
consider h being Function such that
 dom h = NAT and
A1: h . 0 = [F2(),F3(0,F1(),F2()),F3(1,F2(),F3(0,F1(),F2()))] and
A2: for n being Nat holds h . (n + 1) = H2(n,h . n) from NAT_1:sch_11();
deffunc H3( Element of NAT ) ->  set = h . ($1 -' 1);
deffunc H4( set ) ->  set = [F1(),F2(),F3(0,F1(),F2())];
consider g being Function such that
 dom g = NAT and
A3: for x being Element of NAT holds
( ( S1[x] implies g . x = H4(x) ) & ( not S1[x] implies g . x = H3(x) ) ) from PARTFUN1:sch_4();
deffunc H5( set ) ->  set = (g . $1) `1_3 ;
consider f being Function such that
A4: dom f = NAT and
A5: for x being set st x in NAT holds
f . x = H5(x) from FUNCT_1:sch_3();
defpred S2[ Element of NAT ] means ( f . ($1 + 2) = (g . ($1 + 1)) `2_3 & (g . ($1 + 1)) `1_3 = (g . $1) `2_3 & (g . ($1 + 2)) `1_3 = (g . $1) `3_3 & (g . ($1 + 2)) `1_3 = (g . ($1 + 1)) `2_3 & (g . ($1 + 2)) `2_3 = (g . ($1 + 1)) `3_3 & f . ($1 + 2) = F3($1,(f . $1),(f . ($1 + 1))) );
A6: g . 0 = [F1(),F2(),F3(0,F1(),F2())] by A3;
A7: for n being Element of NAT holds g . (n + 2) = H1(n + 1,g . (n + 1))
proof
let n be Element of NAT ; ::_thesis: g . (n + 2) = H1(n + 1,g . (n + 1))
A8: ( (n + 2) - 1 = n + (2 - 1) & 0 <= n + 1 ) by NAT_1:2;
A9: g . (n + 1) = H3(n + 1) by A3
.= h . n by NAT_D:34 ;
thus g . (n + 2) = H3(n + 2) by A3
.= h . (n + 1) by A8, XREAL_0:def_2
.= H1(n + 1,g . (n + 1)) by A2, A9 ; ::_thesis: verum
end;
then A10: (g . (0 + 2)) `2_3 = H1(0 + 1,g . (0 + 1)) `2_3
.= (g . (0 + 1)) `3_3 ;
take  f ; ::_thesis: ( dom f = NAT & f . 0 = F1() & f . 1 = F2() & ( for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
thus  dom f = NAT by A4; ::_thesis: ( f . 0 = F1() & f . 1 = F2() & ( for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
thus A11: f . 0 = (g . 0) `1_3 by A5
.= F1() by A6, Def1 ; ::_thesis: ( f . 1 = F2() & ( for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
A12: g . 1 = H3(1) by A3
.= [F2(),F3(0,F1(),F2()),F3(1,F2(),F3(0,F1(),F2()))] by A1, XREAL_1:232 ;
then A13: (g . (0 + 1)) `1_3 = F2() by Def1
.= (g . 0) `2_3 by A6, Def2 ;
A14: for x being Element of NAT st S2[x] holds
S2[x + 1]
proof
let x be Element of NAT ; ::_thesis: ( S2[x] implies S2[x + 1] )
assume A15: S2[x] ; ::_thesis: S2[x + 1]
then A16: f . (x + 1) = (g . x) `2_3 by A5;
thus A17: f . ((x + 1) + 2) = (g . ((x + 1) + 2)) `1_3 by A5
.= H1((x + 1) + 1,g . ((x + 1) + 1)) `1_3 by A7
.= (g . ((x + 1) + 1)) `2_3 ; ::_thesis: ( (g . ((x + 1) + 1)) `1_3 = (g . (x + 1)) `2_3 & (g . ((x + 1) + 2)) `1_3 = (g . (x + 1)) `3_3 & (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus  (g . ((x + 1) + 1)) `1_3 = (g . (x + 1)) `2_3 by A15; ::_thesis: ( (g . ((x + 1) + 2)) `1_3 = (g . (x + 1)) `3_3 & (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `1_3 = H1((x + 1) + 1,g . ((x + 1) + 1)) `1_3 by A7
.= (g . (x + 1)) `3_3 by A15 ; ::_thesis: ( (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
hence  (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 by A15; ::_thesis: ( (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `2_3 = H1((x + 1) + 1,g . ((x + 1) + 1)) `2_3 by A7
.= (g . ((x + 1) + 1)) `3_3 ; ::_thesis: f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
percases ( x = 0 or x <> 0 ) ;
supposeA18: x = 0 ; ::_thesis: f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
hence f . ((x + 1) + 2) = (g . (1 + 2)) `1_3 by A5
.= H1(1 + 1,g . (1 + 1)) `1_3 by A7
.= (g . (0 + 1)) `3_3 by A15, A18
.= F3(1,F2(),F3(0,F1(),F2())) by A12, Def3
.= F3((0 + 1),F2(),((g . 0) `3_3)) by A6, Def3
.= F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) by A6, A15, A16, A18, Def2 ;
::_thesis: verum
end;
suppose x <> 0 ; ::_thesis: f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
then  0 < x by NAT_1:3;
then A19: 0 + 1 <= x by NAT_1:13;
then A20: (x -' 1) + 1 = x by XREAL_1:235;
 1 - 1 <= x - 1 by A19, XREAL_1:13;
then A21: x - 1 = x -' 1 by XREAL_0:def_2;
 x + 1 = (x - 1) + 2 ;
hence f . ((x + 1) + 2) = H1((x -' 1) + 1,g . ((x -' 1) + 1)) `3_3 by A7, A15, A17, A21
.= F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) by A15, A16, A20 ;
::_thesis: verum
end;
end;
end;
A22: f . (0 + 2) = (g . (0 + 2)) `1_3 by A5
.= H1(0 + 1,g . (0 + 1)) `1_3 by A7
.= (g . (0 + 1)) `2_3 ;
thus A23: f . 1 = (g . 1) `1_3 by A5
.= F2() by A12, Def1 ; ::_thesis: for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1)))
A24: (g . (0 + 2)) `1_3 = H1(0 + 1,g . (0 + 1)) `1_3 by A7
.= (g . 1) `2_3
.= F3(0,F1(),F2()) by A12, Def2
.= (g . 0) `3_3 by A6, Def3 ;
then (g . (0 + 2)) `1_3 = F3(0,F1(),F2()) by A6, Def3
.= (g . (0 + 1)) `2_3 by A12, Def2 ;
then A25: S2[ 0 ] by A12, A11, A23, A22, A13, A24, A10, Def2;
 for x being Element of NAT holds S2[x] from NAT_1:sch_1(A25, A14);
hence  for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ; ::_thesis: verum
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 Element of NAT holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) )
proof
consider f being Function such that
A1: dom f = NAT and
A2: ( f . 0 = F2() & f . 1 = F3() ) and
A3: for n being Element of NAT holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) from RECDEF_2:sch_4();
 rng f c= F1()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in F1() )
assume  y in rng f ; ::_thesis: y in F1()
then consider n being set  such that
A4: n in dom f and
A5: f . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A1, A4;
percases ( n <= 1 or n > 1 ) ;
suppose n <= 1 ; ::_thesis: y in F1()
then  ( n = 0 or n = 1 ) by NAT_1:25;
hence  y in F1() by A2, A5; ::_thesis: verum
end;
suppose n > 1 ; ::_thesis: y in F1()
then  1 + 1 <= n by NAT_1:13;
then  n - 2 is Element of NAT by INT_1:5;
then  f . ((n - 2) + 2) = F4((n - 2),(f . (n - 2)),(f . ((n - 2) + 1))) by A3;
hence  y in F1() by A5; ::_thesis: verum
end;
end;
end;
then  f is Function of NAT,F1() by A1, FUNCT_2:def_1, RELSET_1:4;
hence  ex f being Function of NAT,F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Element of NAT holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) ) by A2, A3; ::_thesis: verum
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 Element of 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 Element of NAT holds F4() . (n + 2) = F5(n,(F4() . n),(F4() . (n + 1)))
proof
defpred S1[ Nat] means F3() . $1 <> F4() . $1;
assume  F3() <> F4() ; ::_thesis: contradiction
then  ex x being set st
( x in NAT & F3() . x <> F4() . x ) by A1, A4, FUNCT_1:2;
then A7: ex k being Nat st S1[k] ;
consider m being Nat such that
A8: S1[m] and
A9: for n being Nat st S1[n] holds
m <= n from NAT_1:sch_5(A7);
now__::_thesis:_(_m_<>_0_implies_not_m_<>_1_)
set k = m -' 2;
A10: ( F3() . ((m -' 2) + 2) = F5((m -' 2),(F3() . (m -' 2)),(F3() . ((m -' 2) + 1))) & F4() . ((m -' 2) + 2) = F5((m -' 2),(F4() . (m -' 2)),(F4() . ((m -' 2) + 1))) ) by A3, A6;
assume  ( m <> 0 & m <> 1 ) ; ::_thesis: contradiction
then  2 <= m by NAT_1:26;
then A11: m = (m -' 2) + 2 by XREAL_1:235;
then A12: F3() . ((m -' 2) + 1) = F4() . ((m -' 2) + 1) by A9, XREAL_1:6;
 (m -' 2) + 0 < m by A11, XREAL_1:6;
hence  contradiction by A8, A9, A11, A12, A10; ::_thesis: verum
end;
hence  contradiction by A2, A5, A8; ::_thesis: verum
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 Element of 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 Element of NAT holds F5() . (n + 2) = F6(n,(F5() . n),(F5() . (n + 1)))
proof
A5: dom F5() = NAT by FUNCT_2:def_1;
A6: dom F4() = NAT by FUNCT_2:def_1;
thus  F4() = F5() from RECDEF_2:sch_6(A6, A1, A2, A5, A3, A4); ::_thesis: verum
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 Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof
defpred S1[ set ] means  In ($1,NAT) > 1;
defpred S2[ set ] means $1 = 1;
defpred S3[ set ] means $1 = 0 ;
deffunc H1( Nat, set ) ->  set = [($2 `2_4),($2 `3_4),($2 `4_4),F4(($1 + 1),($2 `2_4),($2 `3_4),($2 `4_4))];
set r04 = F4(0,F1(),F2(),F3());
set r14 = F4(1,F2(),F3(),F4(0,F1(),F2(),F3()));
set r24 = F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())));
deffunc H2( Nat, set ) ->  set = H1($1 + 2,$2);
consider h being Function such that
 dom h = NAT and
A1: h . 0 = [F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())),F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))] and
A2: for n being Nat holds h . (n + 1) = H2(n,h . n) from NAT_1:sch_11();
deffunc H3( set ) ->  set = h . ((In ($1,NAT)) -' 2);
deffunc H4( set ) ->  set = [F2(),F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))];
deffunc H5( set ) ->  set = [F1(),F2(),F3(),F4(0,F1(),F2(),F3())];
A3: for c being set holds
( not c in NAT or S3[c] or S2[c] or S1[c] )
proof
let c be set ; ::_thesis: ( not c in NAT or S3[c] or S2[c] or S1[c] )
assume  c in NAT ; ::_thesis: ( S3[c] or S2[c] or S1[c] )
then  In (c,NAT) = c by FUNCT_7:def_1;
hence  ( S3[c] or S2[c] or S1[c] ) by NAT_1:25; ::_thesis: verum
end;
A4: for c being set st c in NAT holds
( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) )
proof
let c be set ; ::_thesis: ( c in NAT implies ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) ) )
assume  c in NAT ; ::_thesis: ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) )
then  In (c,NAT) = c by FUNCT_7:def_1;
hence  ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) ) ; ::_thesis: verum
end;
consider g being Function such that
 dom g = NAT and
A5: for x being set st x in NAT holds
( ( S3[x] implies g . x = H5(x) ) & ( S2[x] implies g . x = H4(x) ) & ( S1[x] implies g . x = H3(x) ) ) from RECDEF_2:sch_1(A4, A3);
A6: In (2,NAT) = 2 by FUNCT_7:def_1;
then A7: g . 2 = H3(2) by A5
.= [F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())),F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))] by A1, A6, XREAL_1:232 ;
A8: for n being Element of NAT holds g . (n + 3) = H1(n + 2,g . (n + 2))
proof
let n be Element of NAT ; ::_thesis: g . (n + 3) = H1(n + 2,g . (n + 2))
A9: In ((n + 2),NAT) = n + 2 by FUNCT_7:def_1;
 0 + 1 < n + 2 by NAT_1:2, XREAL_1:8;
then A10: g . (n + 2) = H3(n + 2) by A5, A9
.= h . n by A9, NAT_D:34 ;
A11: In ((n + 3),NAT) = n + 3 by FUNCT_7:def_1;
A12: ( (n + 3) - 2 = n + (3 - 2) & 0 <= n + 1 ) by NAT_1:2;
 0 + 1 < n + 3 by NAT_1:2, XREAL_1:8;
hence g . (n + 3) = H3(n + 3) by A5, A11
.= h . (n + 1) by A11, A12, XREAL_0:def_2
.= H1(n + 2,g . (n + 2)) by A2, A10 ;
::_thesis: verum
end;
A13: g . 1 = [F2(),F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] by A5;
then A14: (g . (0 + 1)) `3_4 = F4(0,F1(),F2(),F3()) by Def6
.= (g . (0 + 2)) `2_4 by A7, Def5 ;
A15: g . 0 = [F1(),F2(),F3(),F4(0,F1(),F2(),F3())] by A5;
then A16: (g . 0) `3_4 = F3() by Def6
.= (g . (0 + 1)) `2_4 by A13, Def5 ;
A17: (g . (0 + 1)) `4_4 = F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) by A13, Def7
.= (g . (0 + 2)) `3_4 by A7, Def6 ;
A18: (g . 0) `4_4 = F4(0,F1(),F2(),F3()) by A15, Def7
.= (g . (0 + 1)) `3_4 by A13, Def6 ;
A19: (g . (0 + 1)) `1_4 = F2() by A13, Def4
.= (g . 0) `2_4 by A15, Def5 ;
deffunc H6( Element of NAT ) ->  set = (g . $1) `1_4 ;
consider f being Function such that
A20: dom f = NAT and
A21: for x being Element of NAT holds f . x = H6(x) from FUNCT_1:sch_4();
A22: f . (0 + 3) = (g . (0 + 3)) `1_4 by A21
.= H1(0 + 2,g . (0 + 2)) `1_4 by A8
.= (g . (0 + 2)) `2_4 ;
take  f ; ::_thesis: ( dom f = NAT & f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus  dom f = NAT by A20; ::_thesis: ( f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
defpred S4[ Element of NAT ] means ( f . ($1 + 3) = (g . ($1 + 2)) `2_4 & (g . $1) `2_4 = (g . ($1 + 1)) `1_4 & (g . $1) `3_4 = (g . ($1 + 1)) `2_4 & (g . $1) `4_4 = (g . ($1 + 1)) `3_4 & (g . ($1 + 1)) `2_4 = (g . ($1 + 2)) `1_4 & (g . ($1 + 1)) `3_4 = (g . ($1 + 2)) `2_4 & (g . ($1 + 1)) `4_4 = (g . ($1 + 2)) `3_4 & (g . ($1 + 2)) `2_4 = (g . ($1 + 3)) `1_4 & f . ($1 + 3) = F4($1,(f . $1),(f . ($1 + 1)),(f . ($1 + 2))) );
A23: (g . (0 + 2)) `2_4 = H1(0 + 2,g . (0 + 2)) `1_4
.= (g . (0 + 3)) `1_4 by A8 ;
thus A24: f . 0 = (g . 0) `1_4 by A21
.= F1() by A15, Def4 ; ::_thesis: ( f . 1 = F2() & f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A25: f . 1 = (g . 1) `1_4 by A21
.= F2() by A13, Def4 ; ::_thesis: ( f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A26: f . 2 = (g . 2) `1_4 by A21
.= F3() by A7, Def4 ; ::_thesis: for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2)))
A27: for x being Element of NAT st S4[x] holds
S4[x + 1]
proof
let x be Element of NAT ; ::_thesis: ( S4[x] implies S4[x + 1] )
A28: (x + 1) + 2 = x + (1 + 2) ;
assume A29: S4[x] ; ::_thesis: S4[x + 1]
then A30: f . ((x + 1) + 1) = (g . x) `3_4 by A21;
thus A31: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A21
.= H1((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by A8
.= (g . ((x + 1) + 2)) `2_4 ; ::_thesis: ( (g . (x + 1)) `2_4 = (g . ((x + 1) + 1)) `1_4 & (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 & (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus  (g . ((x + 1) + 1)) `1_4 = (g . (x + 1)) `2_4 by A29; ::_thesis: ( (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 & (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus  (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 by A29; ::_thesis: ( (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus  (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 by A29; ::_thesis: ( (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `2_4 = H1(x + 2,g . (x + 2)) `1_4
.= (g . ((x + 1) + 2)) `1_4 by A8, A28 ; ::_thesis: ( (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `3_4 = H1(x + 2,g . (x + 2)) `2_4
.= (g . ((x + 1) + 2)) `2_4 by A8, A28 ; ::_thesis: ( (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `4_4 = H1(x + 2,g . (x + 2)) `3_4
.= (g . ((x + 1) + 2)) `3_4 by A8, A28 ; ::_thesis: ( (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 2)) `2_4 = H1((x + 1) + 2,g . ((x + 1) + 2)) `1_4
.= (g . ((x + 1) + 3)) `1_4 by A8 ; ::_thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
percases ( ( x <= 1 & x <> 1 ) or x = 1 or 1 < x ) ;
suppose ( x <= 1 & x <> 1 ) ; ::_thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then A32: x = 0 by NAT_1:25;
hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A21
.= H1(1 + 2,g . (1 + 2)) `1_4 by A8
.= (g . (0 + 3)) `2_4
.= H1(0 + 2,g . (0 + 2)) `2_4 by A8
.= (g . (0 + 2)) `3_4
.= F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) by A7, Def6
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A15, A25, A26, A29, A32, Def7 ;
::_thesis: verum
end;
supposeA33: x = 1 ; ::_thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then A34: ( f . ((x + 1) + 1) = F4(0,F1(),F2(),F3()) & f . ((x + 1) + 2) = F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) ) by A13, A29, A30, Def6, Def7;
thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A21, A33
.= H1(2 + 2,g . (2 + 2)) `1_4 by A8
.= (g . (1 + 3)) `2_4
.= H1(1 + 2,g . (1 + 2)) `2_4 by A8
.= (g . (0 + 3)) `3_4
.= H1(0 + 2,g . (0 + 2)) `3_4 by A8
.= (g . (0 + 2)) `4_4
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A7, A26, A33, A34, Def7 ; ::_thesis: verum
end;
supposeA35: 1 < x ; ::_thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then  1 - 1 <= x - 1 by XREAL_1:13;
then A36: x - 1 = x -' 1 by XREAL_0:def_2;
A37: 1 + 1 <= x by A35, NAT_1:13;
then A38: (x -' 2) + 2 = x by XREAL_1:235;
 2 - 2 <= x - 2 by A37, XREAL_1:13;
then A39: x - 2 = x -' 2 by XREAL_0:def_2;
A40: x + 1 = (x - 1) + 2 ;
thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A31
.= H1(x + 2,g . (x + 2)) `2_4 by A8
.= (g . ((x -' 1) + 3)) `3_4 by A36
.= H1(x + 1,g . (x + 1)) `3_4 by A8, A36, A40
.= (g . ((x -' 2) + 3)) `4_4 by A39
.= H1((x -' 2) + 2,g . ((x -' 2) + 2)) `4_4 by A8
.= F4((x + 1),((g . x) `2_4),((g . x) `3_4),((g . x) `4_4)) by A38
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A21, A29, A30 ; ::_thesis: verum
end;
end;
end;
(g . (0 + 1)) `2_4 = F3() by A13, Def5
.= (g . (0 + 2)) `1_4 by A7, Def4 ;
then A41: S4[ 0 ] by A7, A24, A25, A26, A22, A19, A16, A18, A14, A17, A23, Def5;
 for x being Element of NAT holds S4[x] from NAT_1:sch_1(A41, A27);
hence  for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ; ::_thesis: verum
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 Element of NAT holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof
consider f being Function such that
A1: dom f = NAT and
A2: ( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() ) and
A3: for n being Element of NAT holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) from RECDEF_2:sch_8();
 rng f c= F1()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in F1() )
assume  y in rng f ; ::_thesis: y in F1()
then consider n being set  such that
A4: n in dom f and
A5: f . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A1, A4;
percases ( n <= 2 or n > 2 ) ;
suppose n <= 2 ; ::_thesis: y in F1()
then  ( n = 0 or n = 1 or n = 2 ) by NAT_1:26;
hence  y in F1() by A2, A5; ::_thesis: verum
end;
suppose n > 2 ; ::_thesis: y in F1()
then  2 + 1 <= n by NAT_1:13;
then  n - 3 is Element of NAT by INT_1:5;
then  f . ((n - 3) + 3) = F5((n - 3),(f . (n - 3)),(f . ((n - 3) + 1)),(f . ((n - 3) + 2))) by A3;
hence  y in F1() by A5; ::_thesis: verum
end;
end;
end;
then  f is Function of NAT,F1() by A1, FUNCT_2:def_1, RELSET_1:4;
hence  ex f being Function of NAT,F1() st
( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() & ( for n being Element of NAT holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) ) by A2, A3; ::_thesis: verum
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 Element of 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 Element of NAT holds F5() . (n + 3) = F6(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2)))
proof
defpred S1[ Nat] means F4() . $1 <> F5() . $1;
assume  F4() <> F5() ; ::_thesis: contradiction
then  ex x being set st
( x in NAT & F4() . x <> F5() . x ) by A1, A4, FUNCT_1:2;
then A7: ex k being Nat st S1[k] ;
consider m being Nat such that
A8: S1[m] and
A9: for n being Nat st S1[n] holds
m <= n from NAT_1:sch_5(A7);
now__::_thesis:_(_m_<>_0_&_m_<>_1_implies_not_m_<>_2_)
set k = m -' 3;
A10: ( F4() . ((m -' 3) + 3) = F6((m -' 3),(F4() . (m -' 3)),(F4() . ((m -' 3) + 1)),(F4() . ((m -' 3) + 2))) & F5() . ((m -' 3) + 3) = F6((m -' 3),(F5() . (m -' 3)),(F5() . ((m -' 3) + 1)),(F5() . ((m -' 3) + 2))) ) by A3, A6;
assume  ( m <> 0 & m <> 1 & m <> 2 ) ; ::_thesis: contradiction
then  3 <= m by NAT_1:27;
then A11: m = (m -' 3) + 3 by XREAL_1:235;
then A12: F4() . ((m -' 3) + 1) = F5() . ((m -' 3) + 1) by A9, XREAL_1:6;
A13: F4() . ((m -' 3) + 2) = F5() . ((m -' 3) + 2) by A9, A11, XREAL_1:6;
 (m -' 3) + 0 < m by A11, XREAL_1:6;
hence  contradiction by A8, A9, A11, A12, A13, A10; ::_thesis: verum
end;
hence  contradiction by A2, A5, A8; ::_thesis: verum
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 Element of 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 Element of NAT holds F6() . (n + 3) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)))
proof
A5: dom F6() = NAT by FUNCT_2:def_1;
A6: dom F5() = NAT by FUNCT_2:def_1;
thus  F5() = F6() from RECDEF_2:sch_10(A6, A1, A2, A5, A3, A4); ::_thesis: verum
end;

scheme :: RECDEF_2:sch 12
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 Element of 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 Element of NAT holds F6() . (n + 4) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)),(F6() . (n + 3)))
proof
defpred S1[ Nat] means F5() . $1 <> F6() . $1;
assume  F5() <> F6() ; ::_thesis: contradiction
then  ex x being set st
( x in NAT & F5() . x <> F6() . x ) by A1, A4, FUNCT_1:2;
then A7: ex k being Nat st S1[k] ;
consider m being Nat such that
A8: S1[m] and
A9: for n being Nat st S1[n] holds
m <= n from NAT_1:sch_5(A7);
now__::_thesis:_(_m_<>_0_&_m_<>_1_&_m_<>_2_implies_not_m_<>_3_)
set k = m -' 4;
A10: ( F5() . ((m -' 4) + 4) = F7((m -' 4),(F5() . (m -' 4)),(F5() . ((m -' 4) + 1)),(F5() . ((m -' 4) + 2)),(F5() . ((m -' 4) + 3))) & F6() . ((m -' 4) + 4) = F7((m -' 4),(F6() . (m -' 4)),(F6() . ((m -' 4) + 1)),(F6() . ((m -' 4) + 2)),(F6() . ((m -' 4) + 3))) ) by A3, A6;
assume  ( m <> 0 & m <> 1 & m <> 2 & m <> 3 ) ; ::_thesis: contradiction
then  4 <= m by NAT_1:28;
then A11: m = (m -' 4) + 4 by XREAL_1:235;
then A12: F5() . ((m -' 4) + 1) = F6() . ((m -' 4) + 1) by A9, XREAL_1:6;
 (m -' 4) + 3 < m by A11, XREAL_1:6;
then A13: F5() . ((m -' 4) + 3) = F6() . ((m -' 4) + 3) by A9;
 (m -' 4) + 2 < m by A11, XREAL_1:6;
then A14: F5() . ((m -' 4) + 2) = F6() . ((m -' 4) + 2) by A9;
 (m -' 4) + 0 < m by A11, XREAL_1:6;
hence  contradiction by A8, A9, A11, A12, A14, A13, A10; ::_thesis: verum
end;
hence  contradiction by A2, A5, A8; ::_thesis: verum
end;

scheme :: RECDEF_2:sch 13
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 Element of 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 Element of NAT holds F7() . (n + 4) = F8(n,(F7() . n),(F7() . (n + 1)),(F7() . (n + 2)),(F7() . (n + 3)))
proof
A5: dom F7() = NAT by FUNCT_2:def_1;
A6: dom F6() = NAT by FUNCT_2:def_1;
thus  F6() = F7() from RECDEF_2:sch_12(A6, A1, A2, A5, A3, A4); ::_thesis: verum
end;

begin

theorem :: RECDEF_2:10
for x, y, X, Y, Z being set st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] & x in [:X,Y,Z:] holds
x = y
proof
let x, y, X, Y, Z be set ; ::_thesis: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] & x in [:X,Y,Z:] implies x = y )
assume A1: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] ) ; ::_thesis: ( not x in [:X,Y,Z:] or x = y )
assume  x in [:X,Y,Z:] ; ::_thesis: x = y
hence x = [(x `1_3),(x `2_3),(x `3_3)] by Th3
.= y by A1, Th3 ;
::_thesis: verum
end;