defpred S1[ set ] means $1 = 0 ;
deffunc H1( Nat, set ) -> object = [($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 ) -> object = 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( Nat) -> set = h . ($1 -' 1);
deffunc H4( set ) -> object = [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( object ) -> object = (g . $1) `1_3 ;
consider f being Function such that
A4: dom f = NAT and
A5: for x being object st x in NAT holds
f . x = H5(x) from FUNCT_1:sch 3();
 defpred S2[ 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 Nat holds g . (n + 2) = H1(n + 1,g . (n + 1))
proof
let n be Nat; :: thesis: g . (n + 2) = H1(n + 1,g . (n + 1))
A8: ( (n + 2) - 1 = n + (2 - 1) & 0 <= n + 1 ) ;
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 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 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 ; :: thesis: ( f . 1 = F2() & ( for n being 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()
.= (g . 0) `2_3 by A6 ;
A14: for x being Nat st S2[x] holds
S2[x + 1]
proof
let x be 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)))
per cases ( x = 0 or x <> 0 ) ;
suppose A18: 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
.= F3((0 + 1),F2(),((g . 0) `3_3)) by A6
.= F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) by A6, A15, A16, A18 ;
:: thesis: verum
end;
suppose x <> 0 ; :: thesis: f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
then 0 < x ;
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 ; :: thesis: for n being 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
.= (g . 0) `3_3 by A6 ;
then (g . (0 + 2)) `1_3 = F3(0,F1(),F2()) by A6
.= (g . (0 + 1)) `2_3 by A12 ;
then A25: S2[ 0 ] by A12, A11, A23, A22, A13, A24, A10;
for x being Nat holds S2[x] from NAT_1:sch 2(A25, A14);
 hence for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ; :: thesis: verum