defpred S_{1}[ set ] means $1 = 0 ;

deffunc H_{1}( Nat, set ) -> object = [($2 `2_3),($2 `3_3),F_{3}(($1 + 1),($2 `2_3),($2 `3_3))];

set r03 = F_{3}(0,F_{1}(),F_{2}());

set r13 = F_{3}(1,F_{2}(),F_{3}(0,F_{1}(),F_{2}()));

deffunc H_{2}( Nat, set ) -> object = H_{1}($1 + 1,$2);

consider h being Function such that

dom h = NAT and

A1: h . 0 = [F_{2}(),F_{3}(0,F_{1}(),F_{2}()),F_{3}(1,F_{2}(),F_{3}(0,F_{1}(),F_{2}()))]
and

A2: for n being Nat holds h . (n + 1) = H_{2}(n,h . n)
from NAT_1:sch 11();

deffunc H_{3}( Nat) -> set = h . ($1 -' 1);

deffunc H_{4}( set ) -> object = [F_{1}(),F_{2}(),F_{3}(0,F_{1}(),F_{2}())];

consider g being Function such that

dom g = NAT and

A3: for x being Element of NAT holds

( ( S_{1}[x] implies g . x = H_{4}(x) ) & ( not S_{1}[x] implies g . x = H_{3}(x) ) )
from PARTFUN1:sch 4();

deffunc H_{5}( 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 = H_{5}(x)
from FUNCT_1:sch 3();

defpred S_{2}[ 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_{3}($1,(f . $1),(f . ($1 + 1))) );

A6: g . 0 = [F_{1}(),F_{2}(),F_{3}(0,F_{1}(),F_{2}())]
by A3;

A7: for n being Nat holds g . (n + 2) = H_{1}(n + 1,g . (n + 1))
_{1}(0 + 1,g . (0 + 1)) `2_3

.= (g . (0 + 1)) `3_3 ;

take f ; :: thesis: ( dom f = NAT & f . 0 = F_{1}() & f . 1 = F_{2}() & ( for n being Nat holds f . (n + 2) = F_{3}(n,(f . n),(f . (n + 1))) ) )

thus dom f = NAT by A4; :: thesis: ( f . 0 = F_{1}() & f . 1 = F_{2}() & ( for n being Nat holds f . (n + 2) = F_{3}(n,(f . n),(f . (n + 1))) ) )

thus A11: f . 0 = (g . 0) `1_3 by A5

.= F_{1}()
by A6
; :: thesis: ( f . 1 = F_{2}() & ( for n being Nat holds f . (n + 2) = F_{3}(n,(f . n),(f . (n + 1))) ) )

A12: g . 1 = H_{3}(1)
by A3

.= [F_{2}(),F_{3}(0,F_{1}(),F_{2}()),F_{3}(1,F_{2}(),F_{3}(0,F_{1}(),F_{2}()))]
by A1, XREAL_1:232
;

then A13: (g . (0 + 1)) `1_3 = F_{2}()

.= (g . 0) `2_3 by A6 ;

A14: for x being Nat st S_{2}[x] holds

S_{2}[x + 1]

.= H_{1}(0 + 1,g . (0 + 1)) `1_3
by A7

.= (g . (0 + 1)) `2_3 ;

thus A23: f . 1 = (g . 1) `1_3 by A5

.= F_{2}()
by A12
; :: thesis: for n being Nat holds f . (n + 2) = F_{3}(n,(f . n),(f . (n + 1)))

A24: (g . (0 + 2)) `1_3 = H_{1}(0 + 1,g . (0 + 1)) `1_3
by A7

.= (g . 1) `2_3

.= F_{3}(0,F_{1}(),F_{2}())
by A12

.= (g . 0) `3_3 by A6 ;

then (g . (0 + 2)) `1_3 = F_{3}(0,F_{1}(),F_{2}())
by A6

.= (g . (0 + 1)) `2_3 by A12 ;

then A25: S_{2}[ 0 ]
by A12, A11, A23, A22, A13, A24, A10;

for x being Nat holds S_{2}[x]
from NAT_1:sch 2(A25, A14);

hence for n being Nat holds f . (n + 2) = F_{3}(n,(f . n),(f . (n + 1)))
; :: thesis: verum

deffunc H

set r03 = F

set r13 = F

deffunc H

consider h being Function such that

dom h = NAT and

A1: h . 0 = [F

A2: for n being Nat holds h . (n + 1) = H

deffunc H

deffunc H

consider g being Function such that

dom g = NAT and

A3: for x being Element of NAT holds

( ( S

deffunc H

consider f being Function such that

A4: dom f = NAT and

A5: for x being object st x in NAT holds

f . x = H

defpred S

A6: g . 0 = [F

A7: for n being Nat holds g . (n + 2) = H

proof

then A10: (g . (0 + 2)) `2_3 =
H
let n be Nat; :: thesis: g . (n + 2) = H_{1}(n + 1,g . (n + 1))

A8: ( (n + 2) - 1 = n + (2 - 1) & 0 <= n + 1 ) ;

A9: g . (n + 1) = H_{3}(n + 1)
by A3

.= h . n by NAT_D:34 ;

thus g . (n + 2) = H_{3}(n + 2)
by A3

.= h . (n + 1) by A8, XREAL_0:def 2

.= H_{1}(n + 1,g . (n + 1))
by A2, A9
; :: thesis: verum

end;A8: ( (n + 2) - 1 = n + (2 - 1) & 0 <= n + 1 ) ;

A9: g . (n + 1) = H

.= h . n by NAT_D:34 ;

thus g . (n + 2) = H

.= h . (n + 1) by A8, XREAL_0:def 2

.= H

.= (g . (0 + 1)) `3_3 ;

take f ; :: thesis: ( dom f = NAT & f . 0 = F

thus dom f = NAT by A4; :: thesis: ( f . 0 = F

thus A11: f . 0 = (g . 0) `1_3 by A5

.= F

A12: g . 1 = H

.= [F

then A13: (g . (0 + 1)) `1_3 = F

.= (g . 0) `2_3 by A6 ;

A14: for x being Nat st S

S

proof

A22: f . (0 + 2) =
(g . (0 + 2)) `1_3
by A5
let x be Nat; :: thesis: ( S_{2}[x] implies S_{2}[x + 1] )

assume A15: S_{2}[x]
; :: thesis: S_{2}[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

.= H_{1}((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) = F_{3}((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) = F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )

thus (g . ((x + 1) + 2)) `1_3 = H_{1}((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) = F_{3}((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) = F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )

thus (g . ((x + 1) + 2)) `2_3 = H_{1}((x + 1) + 1,g . ((x + 1) + 1)) `2_3
by A7

.= (g . ((x + 1) + 1)) `3_3 ; :: thesis: f . ((x + 1) + 2) = F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))

end;assume A15: S

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

.= H

.= (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) = F

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) = F

thus (g . ((x + 1) + 2)) `1_3 = H

.= (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) = F

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) = F

thus (g . ((x + 1) + 2)) `2_3 = H

.= (g . ((x + 1) + 1)) `3_3 ; :: thesis: f . ((x + 1) + 2) = F

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

end;

suppose A18:
x = 0
; :: thesis: f . ((x + 1) + 2) = F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))

hence f . ((x + 1) + 2) =
(g . (1 + 2)) `1_3
by A5

.= H_{1}(1 + 1,g . (1 + 1)) `1_3
by A7

.= (g . (0 + 1)) `3_3 by A15, A18

.= F_{3}(1,F_{2}(),F_{3}(0,F_{1}(),F_{2}()))
by A12

.= F_{3}((0 + 1),F_{2}(),((g . 0) `3_3))
by A6

.= F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
by A6, A15, A16, A18
;

:: thesis: verum

end;.= H

.= (g . (0 + 1)) `3_3 by A15, A18

.= F

.= F

.= F

:: thesis: verum

suppose
x <> 0
; :: thesis: f . ((x + 1) + 2) = F_{3}((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) = H_{1}((x -' 1) + 1,g . ((x -' 1) + 1)) `3_3
by A7, A15, A17, A21

.= F_{3}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
by A15, A16, A20
;

:: thesis: verum

end;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) = H

.= F

:: thesis: verum

.= H

.= (g . (0 + 1)) `2_3 ;

thus A23: f . 1 = (g . 1) `1_3 by A5

.= F

A24: (g . (0 + 2)) `1_3 = H

.= (g . 1) `2_3

.= F

.= (g . 0) `3_3 by A6 ;

then (g . (0 + 2)) `1_3 = F

.= (g . (0 + 1)) `2_3 by A12 ;

then A25: S

for x being Nat holds S

hence for n being Nat holds f . (n + 2) = F