defpred S2[ Nat] means ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F4() . \$1 & A = F5() . \$1 & x = F6() . \$1 & P1[S,A,x,\$1] );
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
given S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that A6: ( S = F4() . n & A = F5() . n & x = F6() . n ) and
A7: P1[S,A,x,n] ; :: thesis: S2[n + 1]
take S9 = F1(S,x,n); :: thesis: ex A being non-empty MSAlgebra over S9 ex x being set st
( S9 = F4() . (n + 1) & A = F5() . (n + 1) & x = F6() . (n + 1) & P1[S9,A,x,n + 1] )

reconsider A9 = F2(S,A,x,n) as non-empty MSAlgebra over S9 by A4;
take A9 ; :: thesis: ex x being set st
( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & x = F6() . (n + 1) & P1[S9,A9,x,n + 1] )

take y = F6() . (n + 1); :: thesis: ( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & y = F6() . (n + 1) & P1[S9,A9,y,n + 1] )
y = F3(x,n) by A2, A6;
hence ( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & y = F6() . (n + 1) & P1[S9,A9,y,n + 1] ) by A2, A3, A6, A7; :: thesis: verum
end;
let n be Nat; :: thesis: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )

A8: S2[ 0 ] by A1;
for n being Nat holds S2[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 = F4() . n & A = F5() . n & x = F6() . n & P1[S,A,x,n] ) ;
take S ; :: thesis: ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )

take A ; :: thesis: ( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
thus ( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] ) by A9; :: thesis: verum