defpred S_{2}[ Nat] means ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = F_{4}() . $1 & A = F_{5}() . $1 & x = F_{6}() . $1 & P_{1}[S,A,x,$1] );

A5: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

( S = F_{4}() . n & A = F_{5}() . n & P_{1}[S,A,F_{6}() . n,n] )

A8: S_{2}[ 0 ]
by A1;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A8, A5);

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that

A9: ( S = F_{4}() . n & A = F_{5}() . n & x = F_{6}() . n & P_{1}[S,A,x,n] )
;

take S ; :: thesis: ex A being non-empty MSAlgebra over S st

( S = F_{4}() . n & A = F_{5}() . n & P_{1}[S,A,F_{6}() . n,n] )

take A ; :: thesis: ( S = F_{4}() . n & A = F_{5}() . n & P_{1}[S,A,F_{6}() . n,n] )

thus ( S = F_{4}() . n & A = F_{5}() . n & P_{1}[S,A,F_{6}() . n,n] )
by A9; :: thesis: verum

( S = F

A5: for n being Nat st S

S

proof

let n be Nat; :: thesis: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

given S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that A6: ( S = F_{4}() . n & A = F_{5}() . n & x = F_{6}() . n )
and

A7: P_{1}[S,A,x,n]
; :: thesis: S_{2}[n + 1]

take S9 = F_{1}(S,x,n); :: thesis: ex A being non-empty MSAlgebra over S9 ex x being set st

( S9 = F_{4}() . (n + 1) & A = F_{5}() . (n + 1) & x = F_{6}() . (n + 1) & P_{1}[S9,A,x,n + 1] )

reconsider A9 = F_{2}(S,A,x,n) as non-empty MSAlgebra over S9 by A4;

take A9 ; :: thesis: ex x being set st

( S9 = F_{4}() . (n + 1) & A9 = F_{5}() . (n + 1) & x = F_{6}() . (n + 1) & P_{1}[S9,A9,x,n + 1] )

take y = F_{6}() . (n + 1); :: thesis: ( S9 = F_{4}() . (n + 1) & A9 = F_{5}() . (n + 1) & y = F_{6}() . (n + 1) & P_{1}[S9,A9,y,n + 1] )

y = F_{3}(x,n)
by A2, A6;

hence ( S9 = F_{4}() . (n + 1) & A9 = F_{5}() . (n + 1) & y = F_{6}() . (n + 1) & P_{1}[S9,A9,y,n + 1] )
by A2, A3, A6, A7; :: thesis: verum

end;given S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that A6: ( S = F

A7: P

take S9 = F

( S9 = F

reconsider A9 = F

take A9 ; :: thesis: ex x being set st

( S9 = F

take y = F

y = F

hence ( S9 = F

( S = F

A8: S

for n being Nat holds S

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that

A9: ( S = F

take S ; :: thesis: ex A being non-empty MSAlgebra over S st

( S = F

take A ; :: thesis: ( S = F

thus ( S = F