defpred S₁[ Real] means for p being XFinSequence st len p = $1 holds
P₁[p];
let p be XFinSequence; :: thesis: 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;
for p being XFinSequence st len p = 0 holds
P₁[p]

proof

let p be XFinSequence; :: thesis: ( len p = 0 implies P₁[p] )
assume len p = 0 ; :: thesis: P₁[p]
then p = {} ;
hence P₁[p] by A1; :: thesis: verum

end;

then A4: S₂[ 0 ] by A3;
A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A6: S₂[n] ; :: thesis: S₂[n + 1]
S₁[n + 1]

proof

let p be XFinSequence; :: thesis: ( len p = n + 1 implies P₁[p] )
assume A7: len p = n + 1 ; :: thesis: P₁[p]
then p <> {} ;
then consider w being XFinSequence, x being set such that
A8: p = w ^ <%x%> by Th44;
len p = (len w) + (len <%x%>) by A8, Def4
.= (len w) + 1 by Def5 ;
then P₁[w] by A3, A6, A7;
hence P₁[p] by A8, A2; :: thesis: verum

end;

hence S₂[n + 1] by A3; :: thesis: verum

end;

thus for k being Nat holds S₂[k] from NAT_1:sch 2(A4, A5); :: thesis: verum

end;

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