let p be XFinSequence; :: thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q )
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: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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 that
A3: len p = n + 1 and
A4: 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:40;
A6: n + 1 = (len q) + (len <%x%>) by A3, A5, AFINSQ_1:17
.= (len q) + 1 by AFINSQ_1:33 ;

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:29
.= <%x%> ^ q by A7, AFINSQ_1:29 ;
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 A2, A6;
p = <%y%> ^ (r ^ <%x%>) by A5, A8, AFINSQ_1:27;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; :: thesis: verum

end;

end;

end;

end;

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