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
; 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
; 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
; ( 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 A1, MCART_1:85;
hence
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() )
by A4, A6, A5, A3; 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; 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 ; 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; 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 ; ( 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
; ( 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 A12, MCART_1:85;
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; verum