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

proof

let n be Element of 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 <> <%> F₁() ;
then consider G being XFinSequence of F₁(), d being Element of F₁() such that
A6: F = G ^ <%d%> by Th46;
len <%d%> = 1 by AFINSQ_1:38;
then len F = (len G) + 1 by A6, AFINSQ_1:20;
hence P₁[F] by A2, A4, A5, A6; :: thesis: verum

end;

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