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 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 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 A5: S₂[ 0 ] by A3, A4;
A6: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A7: S₂[n] ; :: thesis: S₂[n + 1]
A8: n + 1 in REAL by XREAL_0:def 1;
S₁[n + 1]

proof

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

end;

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

end;

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

end;

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