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

consider F being Function such that

A1: ( dom F = NAT & F . 0 = [F_{1}(),F_{2}()] )
and

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

deffunc H_{2}( object ) -> object = (F . $1) `2 ;

deffunc H_{3}( object ) -> object = (F . $1) `1 ;

consider f being ManySortedSet of NAT such that

A3: for n being object st n in NAT holds

f . n = H_{3}(n)
from PBOOLE:sch 4();

consider h being ManySortedSet of NAT such that

A4: for n being object st n in NAT holds

h . n = H_{2}(n)
from PBOOLE:sch 4();

take f ; :: thesis: ex h being ManySortedSet of NAT st

( f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

take h ; :: thesis: ( f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

( (F . 0) `1 = F_{1}() & (F . 0) `2 = F_{2}() )
by A1;

hence ( f . 0 = F_{1}() & h . 0 = F_{2}() )
by A3, A4; :: thesis: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) )

let n be Nat; :: thesis: for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) )

let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) )

let x be set ; :: thesis: ( S = f . n & x = h . n implies ( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) )

set x = F . n;

A5: n in NAT by ORDINAL1:def 12;

then A6: h . n = (F . n) `2 by A4;

assume S = f . n ; :: thesis: ( not x = h . n or ( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) )

then S = (F . n) `1 by A3, A5;

then F . (n + 1) = [F_{3}(S,(h . n),n),F_{4}((h . n),n)]
by A2, A6;

then ( (F . (n + 1)) `1 = F_{3}(S,(h . n),n) & (F . (n + 1)) `2 = F_{4}((h . n),n) )
;

hence ( not x = h . n or ( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) )
by A3, A4; :: thesis: verum

consider F being Function such that

A1: ( dom F = NAT & F . 0 = [F

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

deffunc H

deffunc H

consider f being ManySortedSet of NAT such that

A3: for n being object st n in NAT holds

f . n = H

consider h being ManySortedSet of NAT such that

A4: for n being object st n in NAT holds

h . n = H

take f ; :: thesis: ex h being ManySortedSet of NAT st

( f . 0 = F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

take h ; :: thesis: ( f . 0 = F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( (F . 0) `1 = F

hence ( f . 0 = F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

let n be Nat; :: thesis: for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

let x be set ; :: thesis: ( S = f . n & x = h . n implies ( f . (n + 1) = F

set x = F . n;

A5: n in NAT by ORDINAL1:def 12;

then A6: h . n = (F . n) `2 by A4;

assume S = f . n ; :: thesis: ( not x = h . n or ( f . (n + 1) = F

then S = (F . n) `1 by A3, A5;

then F . (n + 1) = [F

then ( (F . (n + 1)) `1 = F

hence ( not x = h . n or ( f . (n + 1) = F