defpred S₁[ set ] means for F being XFinSequence of F₁() st len F = $1 holds
P₁[F];
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A4: for F being XFinSequence of F₁() st len F = n holds
P₁[F] ; :: thesis:
let F be XFinSequence of F₁(); :: thesis:
assume A5: len F = n + 1 ; :: thesis:
then F <> {} ;
then consider G being XFinSequence, d being object such that
A6: F = G ^ <%d%> by AFINSQ_1:40;
reconsider G = G, dd = <%d%> as XFinSequence of F₁() by A6, AFINSQ_1:31;
A7: ( rng dd c= F₁() & rng dd = {d} & d in {d} ) by AFINSQ_1:33, TARSKI:def 1;
len dd = 1 by AFINSQ_1:34;
then len F = (len G) + 1 by A6, AFINSQ_1:17;
hence P₁[F] by A2, A4, A5, A6, A7; :: thesis:

end;