consider D being non empty set ;
reconsider E = D \/ (rng p) as non empty set ;
defpred S₁[ set ] 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 set holds
( x in X iff ( x in E * & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) )
let x be set ; :: 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, XBOOLE_0:def 8;
then ex n being Element of NAT st q = p | (Seg n) by Def1;
then A6: rng q c= rng p by RELAT_1:99;
rng p c= E by XBOOLE_1:7;
then rng q c= E by A6, XBOOLE_1:1;
then reconsider q = q as FinSequence of E by FINSEQ_1:def 4;
q in E * by FINSEQ_1:def 11;
hence x in X by A1, A2, A3; :: thesis: verum