deffunc H1( set , set ) -> object = [[F4((\$2 `11),(\$2 `2),\$1),F5((\$2 `11),(\$2 `12),(\$2 `2),\$1)],F6((\$2 `2),\$1)];
consider F being Function such that
A1: ( dom F = NAT & F . 0 = [[F1(),F2()],F3()] ) and
A2: for n being Nat holds F . (n + 1) = H1(n,F . n) from NAT_1:sch 11();
A3: (F . 0) `2 = F3() by A1;
deffunc H2( object ) -> object = (F . \$1) `2 ;
deffunc H3( object ) -> set = (F . \$1) `12 ;
deffunc H4( 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 = H4(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 = H2(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 = H3(n) from PBOOLE:sch 4();
take f ; :: thesis: ex g, h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )

take g ; :: thesis: ex h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )

take h ; :: thesis: ( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )

( (F . 0) `11 = F1() & (F . 0) `12 = F2() ) by ;
hence ( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() ) 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) )

let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n implies ( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) )
A11: A = (F . n) `12 by A6, A7, A10;
S = (F . n) `11 by A4, A7, A9;
then A12: F . (n + 1) = [[F4(S,(h . n),n),F5(S,A,(h . n),n)],F6((h . n),n)] by A2, A11, A8;
then A13: (F . (n + 1)) `2 = F6((h . n),n) ;
( (F . (n + 1)) `11 = F4(S,(h . n),n) & (F . (n + 1)) `12 = F5(S,A,(h . n),n) ) by ;
hence ( not x = h . n or ( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) by A4, A6, A5, A13; :: thesis: verum