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 Real holds
( x in X iff S₂[x] ) from SUBSET_1:sch 3();
for k being Nat holds k in X

proof

defpred S₃[ Nat] means $1 in X;
A4: S₃[ 0 ]

proof

for q being FinSequence st len q = 0 holds
P₁[q] by A1, Lm4;
hence S₃[ 0 ] by A3; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( n in X implies n + 1 in X )
assume A5: n in X ; :: thesis: n + 1 in X

now

let q be FinSequence; :: thesis: ( len q = n + 1 implies P₁[q] )
assume A6: len q = n + 1 ; :: thesis: P₁[q]
then q <> {} ;
then consider r being FinSequence, x being set such that
A7: q = r ^ <*x*> by Th63;
len q = (len r) + (len <*x*>) by A7, Th35
.= (len r) + 1 by Th56 ;
then P₁[r] by A3, A5, A6;
hence P₁[q] by A2, A7; :: thesis: verum

end;

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

end;

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

end;

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