set r03 = F₃(0 ,F₁(),F₂());
set r13 = F₃(1,F₂(),F₃(0 ,F₁(),F₂()));
deffunc H₁( Nat, set ) -> set = [($2 `2_3 ),($2 `3_3 ),F₃(($1 + 1),($2 `2_3 ),($2 `3_3 ))];
deffunc H₂( Nat, set ) -> set = H₁($1 + 1,$2);
consider h being Function such that
dom h = NAT and
A1: h . 0 = [F₂(),F₃(0 ,F₁(),F₂()),F₃(1,F₂(),F₃(0 ,F₁(),F₂()))] and
A2: for n being Nat holds h . (n + 1) = H₂(n,h . n) from NAT_1:sch 11();
defpred S₁[ set ] means $1 = 0 ;
deffunc H₃( set ) -> set = [F₁(),F₂(),F₃(0 ,F₁(),F₂())];
deffunc H₄( Element of NAT ) -> set = h . ($1 -' 1);
consider g being Function such that
dom g = NAT and
A3: for x being Element of NAT holds
( ( S₁[x] implies g . x = H₃(x) ) & ( not S₁[x] implies g . x = H₄(x) ) ) from PARTFUN1:sch 4();
A4: g . 0 = [F₁(),F₂(),F₃(0 ,F₁(),F₂())] by A3;
A5: g . 1 = H₄(1) by A3
.= [F₂(),F₃(0 ,F₁(),F₂()),F₃(1,F₂(),F₃(0 ,F₁(),F₂()))] by A1, XREAL_1:234 ;
A6: for n being Element of NAT holds g . (n + 2) = H₁(n + 1,g . (n + 1))

proof

let n be Element of NAT ; :: thesis: g . (n + 2) = H₁(n + 1,g . (n + 1))
A7: g . (n + 1) = H₄(n + 1) by A3
.= h . n by NAT_D:34 ;
A8: (n + 2) - 1 = n + (2 - 1) ;
A9: 0 <= n + 1 by NAT_1:2;
thus g . (n + 2) = H₄(n + 2) by A3
.= h . (n + 1) by A8, A9, XREAL_0:def 2
.= H₁(n + 1,g . (n + 1)) by A2, A7 ; :: thesis: verum

end;

deffunc H₅( set ) -> set = (g . $1) `1_3 ;
consider f being Function such that
A10: dom f = NAT and
A11: for x being set st x in NAT holds
f . x = H<sub>5</sub>(x) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = NAT & f . 0 = F<sub>1</sub>() & f . 1 = F<sub>2</sub>() & ( for n being Element of NAT holds f . (n + 2) = F<sub>3</sub>(n,(f . n),(f . (n + 1))) ) )
thus dom f = NAT by A10; :: thesis: ( f . 0 = F<sub>1</sub>() & f . 1 = F<sub>2</sub>() & ( for n being Element of NAT holds f . (n + 2) = F<sub>3</sub>(n,(f . n),(f . (n + 1))) ) )
thus A12: f . 0 = (g . 0 ) `1_3 by A11
.= F₁() by A4, Def1 ; :: thesis: ( f . 1 = F₂() & ( for n being Element of NAT holds f . (n + 2) = F₃(n,(f . n),(f . (n + 1))) ) )
thus A13: f . 1 = (g . 1) `1_3 by A11
.= F<sub>2</sub>() by A5, Def1 ; :: thesis: for n being Element of NAT holds f . (n + 2) = F<sub>3</sub>(n,(f . n),(f . (n + 1)))
defpred S<sub>2</sub>[ 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) = F₃($1,(f . $1),(f . ($1 + 1))) );
A14: S₂[ 0 ]

proof

thus A15: f . (0 + 2) = (g . (0 + 2)) `1_3 by A11
.= H<sub>1</sub>(0 + 1,g . (0 + 1)) `1_3 by A6
.= (g . (0 + 1)) `2_3 by Def1 ; :: thesis: ( (g . (0 + 1)) `1_3 = (g . 0 ) `2_3 & (g . (0 + 2)) `1_3 = (g . 0 ) `3_3 & (g . (0 + 2)) `1_3 = (g . (0 + 1)) `2_3 & (g . (0 + 2)) `2_3 = (g . (0 + 1)) `3_3 & f . (0 + 2) = F<sub>3</sub>(0 ,(f . 0 ),(f . (0 + 1))) )
thus (g . (0 + 1)) `1_3 = F₂() by A5, Def1
.= (g . 0 ) `2_3 by A4, Def2 ; :: thesis: ( (g . (0 + 2)) `1_3 = (g . 0 ) `3_3 & (g . (0 + 2)) `1_3 = (g . (0 + 1)) `2_3 & (g . (0 + 2)) `2_3 = (g . (0 + 1)) `3_3 & f . (0 + 2) = F<sub>3</sub>(0 ,(f . 0 ),(f . (0 + 1))) )
thus (g . (0 + 2)) `1_3 = H₁(0 + 1,g . (0 + 1)) `1_3 by A6
.= (g . 1) `2_3 by Def1
.= F₃(0 ,F₁(),F₂()) by A5, Def2
.= (g . 0 ) `3_3 by A4, Def3 ; :: thesis: ( (g . (0 + 2)) `1_3 = (g . (0 + 1)) `2_3 & (g . (0 + 2)) `2_3 = (g . (0 + 1)) `3_3 & f . (0 + 2) = F<sub>3</sub>(0 ,(f . 0 ),(f . (0 + 1))) )
hence (g . (0 + 2)) `1_3 = F₃(0 ,F₁(),F₂()) by A4, Def3
.= (g . (0 + 1)) `2_3 by A5, Def2 ;
:: thesis: ( (g . (0 + 2)) `2_3 = (g . (0 + 1)) `3_3 & f . (0 + 2) = F<sub>3</sub>(0 ,(f . 0 ),(f . (0 + 1))) )
thus (g . (0 + 2)) `2_3 = H₁(0 + 1,g . (0 + 1)) `2_3 by A6
.= (g . (0 + 1)) `3_3 by Def2 ; :: thesis: f . (0 + 2) = F₃(0 ,(f . 0 ),(f . (0 + 1)))
thus f . (0 + 2) = F₃(0 ,(f . 0 ),(f . (0 + 1))) by A5, A12, A13, A15, Def2; :: thesis: verum

end;

A16: for x being Element of NAT st S₂[x] holds
S₂[x + 1]

proof

let x be Element of NAT ; :: thesis: ( S₂[x] implies S₂[x + 1] )
assume A17: S₂[x] ; :: thesis: S₂[x + 1]
thus A18: f . ((x + 1) + 2) = (g . ((x + 1) + 2)) `1_3 by A11
.= H<sub>1</sub>((x + 1) + 1,g . ((x + 1) + 1)) `1_3 by A6
.= (g . ((x + 1) + 1)) `2_3 by Def1 ; :: 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) = F<sub>3</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 1)) `1_3 = (g . (x + 1)) `2_3 by A17; :: 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) = F<sub>3</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `1_3 = H₁((x + 1) + 1,g . ((x + 1) + 1)) `1_3 by A6
.= (g . (x + 1)) `3_3 by A17, Def1 ; :: 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) = F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
hence (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 by A17; :: thesis: ( (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `2_3 = H<sub>1</sub>((x + 1) + 1,g . ((x + 1) + 1)) `2_3 by A6
.= (g . ((x + 1) + 1)) `3_3 by Def2 ; :: thesis: f . ((x + 1) + 2) = F<sub>3</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
A19: f . (x + 1) = (g . x) `2_3 by A11, A17;

per cases ( x = 0 or x <> 0 ) ;

suppose A20: x = 0 ; :: thesis: f . ((x + 1) + 2) = F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))

hence f . ((x + 1) + 2) = (g . (1 + 2)) `1_3 by A11
.= H<sub>1</sub>(1 + 1,g . (1 + 1)) `1_3 by A6
.= (g . (0 + 1)) `3_3 by A17, A20, Def1
.= F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>())) by A5, Def3
.= F<sub>3</sub>((0 + 1),F<sub>2</sub>(),((g . 0 ) `3_3 )) by A4, Def3
.= F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) by A4, A17, A19, A20, Def2 ;
:: thesis: verum

end;

suppose x <> 0 ; :: thesis: f . ((x + 1) + 2) = F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))

then 0 < x by NAT_1:3;
then A21: 0 + 1 <= x by NAT_1:13;
then 1 - 1 <= x - 1 by XREAL_1:15;
then A22: x - 1 = x -' 1 by XREAL_0:def 2;
A23: x + 1 = (x - 1) + 2 ;
A24: (x -' 1) + 1 = x by A21, XREAL_1:237;
thus f . ((x + 1) + 2) = H₁((x -' 1) + 1,g . ((x -' 1) + 1)) `3_3 by A6, A17, A18, A22, A23
.= F₃((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) by A17, A19, A24, Def3 ; :: thesis: verum

end;

end;

end;

for x being Element of NAT holds S₂[x] from NAT_1:sch 1(A14, A16);
hence for n being Element of NAT holds f . (n + 2) = F₃(n,(f . n),(f . (n + 1))) ; :: thesis: verum