A4:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = F_{6}() . 0 & A = F_{7}() . 0 & x = F_{8}() . 0 & S_{2}[S,A,x, 0 ] )
by A1;

let n be Nat; :: thesis: for S being non empty ManySortedSign

for x being set st S = F_{6}() . n & x = F_{8}() . n holds

( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )

let S be non empty ManySortedSign ; :: thesis: for x being set st S = F_{6}() . n & x = F_{8}() . n holds

( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )

let x be set ; :: thesis: ( S = F_{6}() . n & x = F_{8}() . n implies ( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(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 = F_{6}() . n & A = F_{7}() . n & x = F_{8}() . n & S_{2}[S,A,x,n] holds

S_{2}[F_{3}(S,x,n),F_{4}(S,A,x,n),F_{5}(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 F_{4}(S,A,x,n) is non-empty MSAlgebra over F_{3}(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 = F_{6}() . n & A = F_{7}() . n & x = F_{8}() . n holds

( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{7}() . (n + 1) = F_{4}(S,A,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )
by A2;

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = F_{6}() . n & A = F_{7}() . n & S_{2}[S,A,F_{8}() . 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 = F_{6}() . n & A = F_{7}() . n )
;

assume ( S = F_{6}() . n & x = F_{8}() . n )
; :: thesis: ( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )

hence ( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )
by A2, A8; :: thesis: verum

( S = F

let n be Nat; :: thesis: for S being non empty ManySortedSign

for x being set st S = F

( F

let S be non empty ManySortedSign ; :: thesis: for x being set st S = F

( F

let x be set ; :: thesis: ( S = F

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

S

A6: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

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 = F

( F

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = F

then A8: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = F

assume ( S = F

hence ( F