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 & P₁[S,F₄() . n,n] ) ; :: thesis: S₁[n + 1]
take S' = F₁(S,(F₄() . n),n); :: thesis: ( S' = F₃() . (n + 1) & P₁[S',F₄() . (n + 1),n + 1] )
( F₃() . (n + 1) = F₁(S,(F₄() . n),n) & F₄() . (n + 1) = F₂((F₄() . n),n) ) by A2, A5;
hence ( S' = F₃() . (n + 1) & P₁[S',F₄() . (n + 1),n + 1] ) by A3, A5; :: thesis: verum

end;

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