defpred S1[ Real] means for p being XFinSequence st len p = $1 holds
P1[p];
let p be XFinSequence; :: thesis: P1[p]
consider X being Subset of REAL such that
A2: for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch 3();
 for k being Nat holds k in X
proof
defpred S2[ Nat] means $1 in X;
for p being XFinSequence st len p = 0 holds
P1[p]
proof
let p be XFinSequence; :: thesis: ( len p = 0 implies P1[p] )
assume len p = 0 ; :: thesis: P1[p]
then p = {} ;
hence P1[p] by A1; :: thesis: verum
end;
then A3: S2[ 0 ] by A2;
A4: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A5: S2[n] ; :: thesis: S2[n + 1]
S1[n + 1]
proof
let p be XFinSequence; :: thesis: ( len p = n + 1 implies P1[p] )
assume A8: len p = n + 1 ; :: thesis: P1[p]
then p <> {} ;
then consider w being XFinSequence, x being set such that
A6: p = w ^ <%x%> by Tex;
len p = (len w) + (len <%x%>) by A6, Def4
.= (len w) + 1 by Def5 ;
then P1[w] by A2, A5, A8;
hence P1[p] by A6, A7; :: thesis: verum
end;
hence S2[n + 1] by A2; :: thesis: verum
end;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A3, A4); :: thesis: verum
end;
then len p in X ;
hence P1[p] by A2; :: thesis: verum