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

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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 object st p = <%x%> ^ q )
assume that
A3: len p = n + 1 and
A4: p <> {} ; :: thesis: ex q being XFinSequence ex x being object st p = <%x%> ^ q
consider q being XFinSequence, x being object 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:34 ;

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

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

then p = {} ^ <%x%> by A5
.= <%x%> ^ {} ;
hence ex q being XFinSequence ex x being object st p = <%x%> ^ q ; :: thesis: verum

end;

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

then consider r being XFinSequence, y being object such that
A7: q = <%y%> ^ r by A2, A6;
p = <%y%> ^ (r ^ <%x%>) by A5, A7, AFINSQ_1:27;
hence ex q being XFinSequence ex x being object st p = <%x%> ^ q ; :: thesis: verum

end;

end;

end;

end;

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