A4: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F₆() . 0 & A = F₇() . 0 & x = F₈() . 0 & S₂[S,A,x, 0 ] ) by A1;
let n be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = F₆() . n & x = F₈() . n holds
( F₆() . (n + 1) = F₃(S,x,n) & F₈() . (n + 1) = F₅(x,n) )
let S be non empty ManySortedSign ; :: thesis: for x being set st S = F₆() . n & x = F₈() . n holds
( F₆() . (n + 1) = F₃(S,x,n) & F₈() . (n + 1) = F₅(x,n) )
let x be set ; :: thesis: ( S = F₆() . n & x = F₈() . n implies ( F₆() . (n + 1) = F₃(S,x,n) & F₈() . (n + 1) = F₅(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₆() . n & A = F₇() . n & x = F₈() . n & S₂[S,A,x,n] holds
S₂[F₃(S,x,n),F₄(S,A,x,n),F₅(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₄(S,A,x,n) is non-empty MSAlgebra over F₃(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₆() . n & A = F₇() . n & x = F₈() . n holds
( F₆() . (n + 1) = F₃(S,x,n) & F₇() . (n + 1) = F₄(S,A,x,n) & F₈() . (n + 1) = F₅(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₆() . n & A = F₇() . n & S₂[S,A,F₈() . 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₆() . n & A = F₇() . n ) ;
assume ( S = F₆() . n & x = F₈() . n ) ; :: thesis: ( F₆() . (n + 1) = F₃(S,x,n) & F₈() . (n + 1) = F₅(x,n) )
hence ( F₆() . (n + 1) = F₃(S,x,n) & F₈() . (n + 1) = F₅(x,n) ) by A2, A8; :: thesis: verum