defpred S_{1}[ object ] means In ($1,NAT) > 1;

defpred S_{2}[ object ] means $1 = 1;

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

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

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

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

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

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

consider h being Function such that

dom h = NAT and

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

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

deffunc H_{3}( object ) -> set = h . ((In ($1,NAT)) -' 2);

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

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

A3: for c being set holds

( not c in NAT or S_{3}[c] or S_{2}[c] or S_{1}[c] )

( ( S_{3}[c] implies not S_{2}[c] ) & ( S_{3}[c] implies not S_{1}[c] ) & ( S_{2}[c] implies not S_{1}[c] ) )
;

consider g being Function such that

dom g = NAT and

A5: for x being set st x in NAT holds

( ( S_{3}[x] implies g . x = H_{5}(x) ) & ( S_{2}[x] implies g . x = H_{4}(x) ) & ( S_{1}[x] implies g . x = H_{3}(x) ) )
from RECDEF_2:sch 1(A4, A3);

A6: g . 2 = H_{3}(2)
by A5

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

A7: for n being Nat holds g . (n + 3) = H_{1}(n + 2,g . (n + 2))
_{2}(),F_{3}(),F_{4}(0,F_{1}(),F_{2}(),F_{3}()),F_{4}(1,F_{2}(),F_{3}(),F_{4}(0,F_{1}(),F_{2}(),F_{3}()))]
by A5;

then A11: (g . (0 + 1)) `3_4 = F_{4}(0,F_{1}(),F_{2}(),F_{3}())

.= (g . (0 + 2)) `2_4 by A6 ;

A12: g . 0 = [F_{1}(),F_{2}(),F_{3}(),F_{4}(0,F_{1}(),F_{2}(),F_{3}())]
by A5;

then A13: (g . 0) `3_4 = F_{3}()

.= (g . (0 + 1)) `2_4 by A10 ;

A14: (g . (0 + 1)) `4_4 = F_{4}(1,F_{2}(),F_{3}(),F_{4}(0,F_{1}(),F_{2}(),F_{3}()))
by A10

.= (g . (0 + 2)) `3_4 by A6 ;

A15: (g . 0) `4_4 = F_{4}(0,F_{1}(),F_{2}(),F_{3}())
by A12

.= (g . (0 + 1)) `3_4 by A10 ;

A16: (g . (0 + 1)) `1_4 = F_{2}()
by A10

.= (g . 0) `2_4 by A12 ;

deffunc H_{6}( Nat) -> object = (g . $1) `1_4 ;

consider f being Function such that

A17: dom f = NAT and

A18: for x being Element of NAT holds f . x = H_{6}(x)
from FUNCT_1:sch 4();

A19: f . (0 + 3) = (g . (0 + 3)) `1_4 by A18

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

.= (g . (0 + 2)) `2_4 ;

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

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

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

A20: (g . (0 + 2)) `2_4 = H_{1}(0 + 2,g . (0 + 2)) `1_4

.= (g . (0 + 3)) `1_4 by A7 ;

thus A21: f . 0 = (g . 0) `1_4 by A18

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

thus A22: f . 1 = (g . 1) `1_4 by A18

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

thus A23: f . 2 = (g . 2) `1_4 by A18

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

A24: for x being Nat st S_{4}[x] holds

S_{4}[x + 1]
_{3}()
by A10

.= (g . (0 + 2)) `1_4 by A6 ;

then A38: S_{4}[ 0 ]
by A6, A21, A22, A23, A19, A16, A13, A15, A11, A14, A20;

for x being Nat holds S_{4}[x]
from NAT_1:sch 2(A38, A24);

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

defpred S

defpred S

deffunc H

set r04 = F

set r14 = F

set r24 = 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

deffunc H

A3: for c being set holds

( not c in NAT or S

proof

A4:
for c being set st c in NAT holds
let c be set ; :: thesis: ( not c in NAT or S_{3}[c] or S_{2}[c] or S_{1}[c] )

assume c in NAT ; :: thesis: ( S_{3}[c] or S_{2}[c] or S_{1}[c] )

then In (c,NAT) = c by SUBSET_1:def 8;

hence ( S_{3}[c] or S_{2}[c] or S_{1}[c] )
by NAT_1:25; :: thesis: verum

end;assume c in NAT ; :: thesis: ( S

then In (c,NAT) = c by SUBSET_1:def 8;

hence ( S

( ( S

consider g being Function such that

dom g = NAT and

A5: for x being set st x in NAT holds

( ( S

A6: g . 2 = H

.= [F

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

proof

A10:
g . 1 = [F
let n be Nat; :: thesis: g . (n + 3) = H_{1}(n + 2,g . (n + 2))

0 + 1 < n + 2 by XREAL_1:8;

then A8: g . (n + 2) = H_{3}(n + 2)
by A5

.= h . n by NAT_D:34 ;

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

0 + 1 < n + 3 by XREAL_1:8;

hence g . (n + 3) = H_{3}(n + 3)
by A5

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

.= H_{1}(n + 2,g . (n + 2))
by A2, A8
;

:: thesis: verum

end;0 + 1 < n + 2 by XREAL_1:8;

then A8: g . (n + 2) = H

.= h . n by NAT_D:34 ;

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

0 + 1 < n + 3 by XREAL_1:8;

hence g . (n + 3) = H

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

.= H

:: thesis: verum

then A11: (g . (0 + 1)) `3_4 = F

.= (g . (0 + 2)) `2_4 by A6 ;

A12: g . 0 = [F

then A13: (g . 0) `3_4 = F

.= (g . (0 + 1)) `2_4 by A10 ;

A14: (g . (0 + 1)) `4_4 = F

.= (g . (0 + 2)) `3_4 by A6 ;

A15: (g . 0) `4_4 = F

.= (g . (0 + 1)) `3_4 by A10 ;

A16: (g . (0 + 1)) `1_4 = F

.= (g . 0) `2_4 by A12 ;

deffunc H

consider f being Function such that

A17: dom f = NAT and

A18: for x being Element of NAT holds f . x = H

A19: f . (0 + 3) = (g . (0 + 3)) `1_4 by A18

.= H

.= (g . (0 + 2)) `2_4 ;

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

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

defpred S

A20: (g . (0 + 2)) `2_4 = H

.= (g . (0 + 3)) `1_4 by A7 ;

thus A21: f . 0 = (g . 0) `1_4 by A18

.= F

thus A22: f . 1 = (g . 1) `1_4 by A18

.= F

thus A23: f . 2 = (g . 2) `1_4 by A18

.= F

A24: for x being Nat st S

S

proof

(g . (0 + 1)) `2_4 =
F
let x be Nat; :: thesis: ( S_{4}[x] implies S_{4}[x + 1] )

A25: (x + 1) + 2 = x + (1 + 2) ;

assume A26: S_{4}[x]
; :: thesis: S_{4}[x + 1]

then A27: f . ((x + 1) + 1) = (g . x) `3_4 by A18;

thus A28: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A18

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

.= (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) = F_{4}((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 A26; :: 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) = F_{4}((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 A26; :: 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) = F_{4}((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 A26; :: 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) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )

thus (g . ((x + 1) + 1)) `2_4 = H_{1}(x + 2,g . (x + 2)) `1_4

.= (g . ((x + 1) + 2)) `1_4 by A7, A25 ; :: 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) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )

thus (g . ((x + 1) + 1)) `3_4 = H_{1}(x + 2,g . (x + 2)) `2_4

.= (g . ((x + 1) + 2)) `2_4 by A7, A25 ; :: 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) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )

thus (g . ((x + 1) + 1)) `4_4 = H_{1}(x + 2,g . (x + 2)) `3_4

.= (g . ((x + 1) + 2)) `3_4 by A7, A25 ; :: thesis: ( (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )

thus (g . ((x + 1) + 2)) `2_4 = H_{1}((x + 1) + 2,g . ((x + 1) + 2)) `1_4

.= (g . ((x + 1) + 3)) `1_4 by A7 ; :: thesis: f . ((x + 1) + 3) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

end;A25: (x + 1) + 2 = x + (1 + 2) ;

assume A26: S

then A27: f . ((x + 1) + 1) = (g . x) `3_4 by A18;

thus A28: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A18

.= H

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

thus (g . ((x + 1) + 1)) `1_4 = (g . (x + 1)) `2_4 by A26; :: 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) = F

thus (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 by A26; :: 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) = F

thus (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 by A26; :: 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) = F

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

.= (g . ((x + 1) + 2)) `1_4 by A7, A25 ; :: 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) = F

thus (g . ((x + 1) + 1)) `3_4 = H

.= (g . ((x + 1) + 2)) `2_4 by A7, A25 ; :: 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) = F

thus (g . ((x + 1) + 1)) `4_4 = H

.= (g . ((x + 1) + 2)) `3_4 by A7, A25 ; :: thesis: ( (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F

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

.= (g . ((x + 1) + 3)) `1_4 by A7 ; :: thesis: f . ((x + 1) + 3) = F

per cases
( ( x <= 1 & x <> 1 ) or x = 1 or 1 < x )
;

end;

suppose
( x <= 1 & x <> 1 )
; :: thesis: f . ((x + 1) + 3) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

then A29:
x = 0
by NAT_1:25;

hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A18

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

.= (g . (0 + 3)) `2_4

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

.= (g . (0 + 2)) `3_4

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

.= F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
by A12, A22, A23, A26, A29
;

:: thesis: verum

end;hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A18

.= H

.= (g . (0 + 3)) `2_4

.= H

.= (g . (0 + 2)) `3_4

.= F

.= F

:: thesis: verum

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

then A31:
( f . ((x + 1) + 1) = F_{4}(0,F_{1}(),F_{2}(),F_{3}()) & f . ((x + 1) + 2) = F_{4}(1,F_{2}(),F_{3}(),F_{4}(0,F_{1}(),F_{2}(),F_{3}())) )
by A10, A26, A27;

thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A18, A30

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

.= (g . (1 + 3)) `2_4

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

.= (g . (0 + 3)) `3_4

.= H_{1}(0 + 2,g . (0 + 2)) `3_4
by A7

.= (g . (0 + 2)) `4_4

.= F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
by A6, A23, A30, A31
; :: thesis: verum

end;thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A18, A30

.= H

.= (g . (1 + 3)) `2_4

.= H

.= (g . (0 + 3)) `3_4

.= H

.= (g . (0 + 2)) `4_4

.= F

suppose A32:
1 < x
; :: thesis: f . ((x + 1) + 3) = F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

then
1 - 1 <= x - 1
by XREAL_1:13;

then A33: x - 1 = x -' 1 by XREAL_0:def 2;

A34: 1 + 1 <= x by A32, NAT_1:13;

then A35: (x -' 2) + 2 = x by XREAL_1:235;

2 - 2 <= x - 2 by A34, XREAL_1:13;

then A36: x - 2 = x -' 2 by XREAL_0:def 2;

A37: x + 1 = (x - 1) + 2 ;

thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A28

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

.= (g . ((x -' 1) + 3)) `3_4 by A33

.= H_{1}(x + 1,g . (x + 1)) `3_4
by A7, A33, A37

.= (g . ((x -' 2) + 3)) `4_4 by A36

.= H_{1}((x -' 2) + 2,g . ((x -' 2) + 2)) `4_4
by A7

.= F_{4}((x + 1),((g . x) `2_4),((g . x) `3_4),((g . x) `4_4))
by A35

.= F_{4}((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
by A18, A26, A27
; :: thesis: verum

end;then A33: x - 1 = x -' 1 by XREAL_0:def 2;

A34: 1 + 1 <= x by A32, NAT_1:13;

then A35: (x -' 2) + 2 = x by XREAL_1:235;

2 - 2 <= x - 2 by A34, XREAL_1:13;

then A36: x - 2 = x -' 2 by XREAL_0:def 2;

A37: x + 1 = (x - 1) + 2 ;

thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A28

.= H

.= (g . ((x -' 1) + 3)) `3_4 by A33

.= H

.= (g . ((x -' 2) + 3)) `4_4 by A36

.= H

.= F

.= F

.= (g . (0 + 2)) `1_4 by A6 ;

then A38: S

for x being Nat holds S

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