A4: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F6() . 0 & A = F7() . 0 & x = F8() . 0 & S2[S,A,x, 0 ] ) by A1;
let n be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = F6() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )

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

let x be set ; :: thesis: ( S = F6() . n & x = F8() . n implies ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) ) )
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 = F6() . n & A = F7() . n & x = F8() . n & S2[S,A,x,n] holds
S2[F3(S,x,n),F4(S,A,x,n),F5(x,n),n + 1] ;
A6: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F4(S,A,x,n) is non-empty MSAlgebra over F3(S,x,n) by A3;
A7: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F6() . n & A = F7() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F7() . (n + 1) = F4(S,A,x,n) & F8() . (n + 1) = F5(x,n) ) by A2;
for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F6() . n & A = F7() . n & S2[S,A,F8() . n,n] ) from CIRCCMB2:sch 13(A4, A7, A5, A6);
then A8: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F6() . n & A = F7() . n ) ;
assume ( S = F6() . n & x = F8() . n ) ; :: thesis: ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
hence ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) ) by A2, A8; :: thesis: verum