A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F₅(S,A,x,n) is non-empty MSAlgebra over F₄(S,x,n) by A1;
consider f, g, h being ManySortedSet of NAT such that
A3: ( f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() ) and
A4: 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) from CIRCCMB2:sch 12();
A5: 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 & S₂[S,A,x,n] holds
S₂[F₄(S,x,n),F₅(S,A,x,n),F₆(x,n),n + 1] ;
A6: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S₂[S,A,x, 0 ] ) by A3;
for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S₂[S,A,h . n,n] ) from CIRCCMB2:sch 13(A6, A4, A5, A2);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A7: ( S = f . F₇() & A = g . F₇() ) ;
take S ; :: thesis: ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st
( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take A ; :: thesis: ex f, g, h being ManySortedSet of NAT st
( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take f ; :: thesis: ex g, h being ManySortedSet of NAT st
( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take g ; :: thesis: ex h being ManySortedSet of NAT st
( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
take h ; :: thesis: ( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )
thus ( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) ) by A3, A4, A7; :: thesis: verum