deffunc H_{1}( set , set ) -> object = [[F_{4}(($2 `11),($2 `2),$1),F_{5}(($2 `11),($2 `12),($2 `2),$1)],F_{6}(($2 `2),$1)];

consider F being Function such that

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

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

A3: (F . 0) `2 = F_{3}()
by A1;

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

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

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

consider f being ManySortedSet of NAT such that

A4: for n being object st n in NAT holds

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

consider h being ManySortedSet of NAT such that

A5: for n being object st n in NAT holds

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

consider g being ManySortedSet of NAT such that

A6: for n being object st n in NAT holds

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

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

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

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

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

( (F . 0) `11 = F_{1}() & (F . 0) `12 = F_{2}() )
by A1, MCART_1:85;

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) )

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

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) )

let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) )

let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) )

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

set x = F . n;

A7: n in NAT by ORDINAL1:def 12;

then A8: h . n = (F . n) `2 by A5;

assume that

A9: S = f . n and

A10: A = g . n ; :: thesis: ( not x = h . n or ( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) )

A11: A = (F . n) `12 by A6, A7, A10;

S = (F . n) `11 by A4, A7, A9;

then A12: F . (n + 1) = [[F_{4}(S,(h . n),n),F_{5}(S,A,(h . n),n)],F_{6}((h . n),n)]
by A2, A11, A8;

then A13: (F . (n + 1)) `2 = F_{6}((h . n),n)
;

( (F . (n + 1)) `11 = F_{4}(S,(h . n),n) & (F . (n + 1)) `12 = F_{5}(S,A,(h . n),n) )
by A12, MCART_1:85;

hence ( not x = h . n or ( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) )
by A4, A6, A5, A13; :: 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

A3: (F . 0) `2 = F

deffunc H

deffunc H

deffunc H

consider f being ManySortedSet of NAT such that

A4: for n being object st n in NAT holds

f . n = H

consider h being ManySortedSet of NAT such that

A5: for n being object st n in NAT holds

h . n = H

consider g being ManySortedSet of NAT such that

A6: for n being object st n in NAT holds

g . n = H

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

( f . 0 = F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

( f . 0 = F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

( (F . 0) `11 = F

hence ( f . 0 = F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F

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

set x = F . n;

A7: n in NAT by ORDINAL1:def 12;

then A8: h . n = (F . n) `2 by A5;

assume that

A9: S = f . n and

A10: A = g . n ; :: thesis: ( not x = h . n or ( f . (n + 1) = F

A11: A = (F . n) `12 by A6, A7, A10;

S = (F . n) `11 by A4, A7, A9;

then A12: F . (n + 1) = [[F

then A13: (F . (n + 1)) `2 = F

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

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