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

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

( (F . 0) `1 = F1() & (F . 0) `2 = F2() ) by A1;
hence ( f . 0 = F1() & h . 0 = F2() ) 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) = F3(S,x,n) & h . (n + 1) = F4(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) = F3(S,x,n) & h . (n + 1) = F4(x,n) )

let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )

let x be set ; :: thesis: ( S = f . n & x = h . n implies ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(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) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
then S = (F . n) `1 by A3, A5;
then F . (n + 1) = [F3(S,(h . n),n),F4((h . n),n)] by A2, A6;
then ( (F . (n + 1)) `1 = F3(S,(h . n),n) & (F . (n + 1)) `2 = F4((h . n),n) ) ;
hence ( not x = h . n or ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) by A3, A4; :: thesis: verum