defpred S₂[ Nat] means ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F₄() . $1 & A = F₅() . $1 & x = F₆() . $1 & P₁[S,A,x,$1] );
A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
given S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set such that A6: ( S = F₄() . n & A = F₅() . n & x = F₆() . n ) and
A7: P₁[S,A,x,n] ; :: thesis: S₂[n + 1]
take S9 = F₁(S,x,n); :: thesis: ex A being non-empty MSAlgebra over S9 ex x being set st
( S9 = F₄() . (n + 1) & A = F₅() . (n + 1) & x = F₆() . (n + 1) & P₁[S9,A,x,n + 1] )
reconsider A9 = F₂(S,A,x,n) as non-empty MSAlgebra over S9 by A4;
take A9 ; :: thesis: ex x being set st
( S9 = F₄() . (n + 1) & A9 = F₅() . (n + 1) & x = F₆() . (n + 1) & P₁[S9,A9,x,n + 1] )
take y = F₆() . (n + 1); :: thesis: ( S9 = F₄() . (n + 1) & A9 = F₅() . (n + 1) & y = F₆() . (n + 1) & P₁[S9,A9,y,n + 1] )
y = F₃(x,n) by A2, A6;
hence ( S9 = F₄() . (n + 1) & A9 = F₅() . (n + 1) & y = F₆() . (n + 1) & P₁[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 = F₄() . n & A = F₅() . n & P₁[S,A,F₆() . n,n] )
A8: S₂[ 0 ] by A1;
for n being Nat holds S₂[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₄() . n & A = F₅() . n & x = F₆() . n & P₁[S,A,x,n] ) ;
take S ; :: thesis: ex A being non-empty MSAlgebra over S st
( S = F₄() . n & A = F₅() . n & P₁[S,A,F₆() . n,n] )
take A ; :: thesis: ( S = F₄() . n & A = F₅() . n & P₁[S,A,F₆() . n,n] )
thus ( S = F₄() . n & A = F₅() . n & P₁[S,A,F₆() . n,n] ) by A9; :: thesis: verum