set E = rng p;
defpred S₁[ object ] means ex q being FinSequence st
( $1 = q & q is_a_proper_prefix_of p );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in (rng p) * & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being object holds
( x in X iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
let x be object ; :: thesis: ( x in X iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
thus ( x in X implies ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) by A1; :: thesis: ( ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) implies x in X )
given q being FinSequence such that A2: x = q and
A3: q is_a_proper_prefix_of p ; :: thesis: x in X
q is_a_prefix_of p by A3;
then ex n being Nat st q = p | (Seg n) ;
then rng q c= rng p by RELAT_1:70;
then reconsider q = q as FinSequence of rng p by FINSEQ_1:def 4;
q in (rng p) * by FINSEQ_1:def 11;
hence x in X by A1, A2, A3; :: thesis: verum