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
A4: q is_a_prefix_of p by A3, XBOOLE_0:def 8;
A5: ex n being Element of NAT st q = p | (Seg n) by A4, Def1;
A6: rng q c= rng p by A5, RELAT_1:99;
A7: rng p c= E by XBOOLE_1:7;
A8: rng q c= E by A6, A7, XBOOLE_1:1;
reconsider q = q as FinSequence of E by A8, FINSEQ_1:def 4;
A9: q in E * by FINSEQ_1:def 11;
thus x in X by A1, A2, A3, A9; :: thesis: verum