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]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: for F being XFinSequence of F₁() st len F = n holds
P₁[F] ; :: thesis: S₁[n + 1]
let F be XFinSequence of F₁(); :: thesis: ( len F = n + 1 implies P₁[F] )
assume A5: len F = n + 1 ; :: thesis: P₁[F]
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: verum

end;

let F be XFinSequence of F₁(); :: thesis: P₁[F]
A8: len F = len F ;
for X being set st card X = {} holds
X = {} ;
then A9: S₁[ 0 ] by A1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A3);
hence P₁[F] by A8; :: thesis: verum