consider f, h being ManySortedSet of NAT such that
A1:
( f . 0 = F1() & h . 0 = F2() )
and
A2:
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) )
from CIRCCMB2:sch 1();
A3:
for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1]
;
A4:
ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = h . 0 & S1[S,x, 0 ] )
by A1;
for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S1[S,h . n,n] )
from CIRCCMB2:sch 2(A4, A2, A3);
then consider S being non empty ManySortedSign such that
A5:
S = f . F5()
;
take
S
; ex f, h being ManySortedSet of NAT st
( S = f . F5() & 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
f
; ex h being ManySortedSet of NAT st
( S = f . F5() & 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
; ( S = f . F5() & 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) ) ) )
thus
( S = f . F5() & 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) ) ) )
by A1, A2, A5; verum