defpred S₁[ Nat] means for p being XFinSequence st len p = $1 & p <> {} holds
ex q being XFinSequence ex x being set st p = <%x%> ^ q;
A1: S₁[ 0 ] ;

A2: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let p be XFinSequence; :: thesis: ( len p = n + 1 & p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q )
assume A4: ( len p = n + 1 & p <> {} ) ; :: thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
consider q being XFinSequence, x being set such that
A5: p = q ^ <%x%> by A4, AFINSQ_1:44;
A6: n + 1 = (len q) + (len <%x%>) by A4, A5, AFINSQ_1:20
.= (len q) + 1 by AFINSQ_1:36 ;

per cases ( q = {} or q <> {} ) ;

suppose A7: q = {} ; :: thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q

then p = <%x%> by A5, AFINSQ_1:32
.= <%x%> ^ q by A7, AFINSQ_1:32 ;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; :: thesis: verum

end;

suppose q <> {} ; :: thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q

then consider r being XFinSequence, y being set such that
A8: q = <%y%> ^ r by A3, A6;
p = <%y%> ^ (r ^ <%x%>) by A5, A8, AFINSQ_1:30;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; :: thesis: verum

end;

end;

end;

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let p be XFinSequence; :: thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q )
assume A10: p <> {} ; :: thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
len p = len p ;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q by A9, A10; :: thesis: verum