defpred S₁[ Nat] means ex S being non empty ManySortedSign st
( S = F₃() . $1 & P₁[S,F₄() . $1,$1] );
A4: 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 such that A5: S = F₃() . n and
A6: P₁[S,F₄() . n,n] ; :: thesis: S₁[n + 1]
take F₁(S,(F₄() . n),n) ; :: thesis: ( F₁(S,(F₄() . n),n) = F₃() . (n + 1) & P₁[F₁(S,(F₄() . n),n),F₄() . (n + 1),n + 1] )
F₄() . (n + 1) = F₂((F₄() . n),n) by A2, A5;
hence ( F₁(S,(F₄() . n),n) = F₃() . (n + 1) & P₁[F₁(S,(F₄() . n),n),F₄() . (n + 1),n + 1] ) by A2, A3, A5, A6; :: thesis: verum

end;

A7: S₁[ 0 ] by A1;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A4); :: thesis: verum