let p be FinSequence; :: thesis: P₁[p]
defpred S₂[ set ] means for p being FinSequence st len p = $1 holds
P₁[p];
consider X being Subset of REAL such that
A3: for x being Element of REAL holds
( x in X iff S₂[x] ) from SUBSET_1:sch 3();
for k being Nat holds k in X

proof

A4: 0 in REAL by XREAL_0:def 1;
defpred S₃[ Nat] means $1 in X;
for q being FinSequence st len q = 0 holds
P₁[q] by A1, Lm3;
then A5: S₃[ 0 ] by A3, A4;

now :: thesis: for n being Nat st n in X holds
n + 1 in X

let n be Nat; :: thesis: ( n in X implies n + 1 in X )
assume A6: n in X ; :: thesis: n + 1 in X
A7: n + 1 in REAL by NUMBERS:19;

now :: thesis: for q being FinSequence st len q = n + 1 holds
P₁[q]

let q be FinSequence; :: thesis: ( len q = n + 1 implies P₁[q] )
assume A8: len q = n + 1 ; :: thesis: P₁[q]
then q <> {} ;
then consider r being FinSequence, x being object such that
A9: q = r ^ <*x*> by Th46;
len q = (len r) + (len <*x*>) by A9, Th22
.= (len r) + 1 by Th39 ;
hence P₁[q] by A2, A9, A3, A6, A8; :: thesis: verum

end;

hence n + 1 in X by A3, A7; :: thesis: verum

end;

then A10: for n being Nat st S₃[n] holds
S₃[n + 1] ;
thus for n being Nat holds S₃[n] from NAT_1:sch 2(A5, A10); :: thesis: verum

end;

then len p in X ;
hence P₁[p] by A3; :: thesis: verum