let x be set ; :: thesis: for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}
let v be FinSequence; :: thesis: ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v}
thus ProperPrefixes (v ^ <*x*>) c= (ProperPrefixes v) \/ {v} :: according to XBOOLE_0:def 10 :: thesis: (ProperPrefixes v) \/ {v} c= ProperPrefixes (v ^ <*x*>)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ProperPrefixes (v ^ <*x*>) or y in (ProperPrefixes v) \/ {v} )
assume y in ProperPrefixes (v ^ <*x*>) ; :: thesis: y in (ProperPrefixes v) \/ {v}
then consider v1 being FinSequence such that
A1: y = v1 and
A2: v1 is_a_proper_prefix_of v ^ <*x*> by TREES_1:def 2;
( ( v1 is_a_prefix_of v & v1 <> v ) or v1 = v ) by A2, TREES_1:9;
then ( v1 is_a_proper_prefix_of v or v1 in {v} ) by TARSKI:def 1;
then ( y in ProperPrefixes v or y in {v} ) by A1, TREES_1:def 2;
hence y in (ProperPrefixes v) \/ {v} by XBOOLE_0:def 3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (ProperPrefixes v) \/ {v} or y in ProperPrefixes (v ^ <*x*>) )
assume y in (ProperPrefixes v) \/ {v} ; :: thesis: y in ProperPrefixes (v ^ <*x*>)
then A3: ( y in ProperPrefixes v or y in {v} ) by XBOOLE_0:def 3;

A4: now :: thesis: ( y in ProperPrefixes v implies y in ProperPrefixes (v ^ <*x*>) )

assume y in ProperPrefixes v ; :: thesis: y in ProperPrefixes (v ^ <*x*>)
then consider v1 being FinSequence such that
A5: y = v1 and
A6: v1 is_a_proper_prefix_of v by TREES_1:def 2;
v is_a_prefix_of v ^ <*x*> by TREES_1:1;
then v1 is_a_proper_prefix_of v ^ <*x*> by A6, XBOOLE_1:58;
hence y in ProperPrefixes (v ^ <*x*>) by A5, TREES_1:def 2; :: thesis: verum

end;

v ^ {} = v by FINSEQ_1:34;
then ( v is_a_prefix_of v ^ <*x*> & v <> v ^ <*x*> ) by FINSEQ_1:33, TREES_1:1;
then v is_a_proper_prefix_of v ^ <*x*> ;
then ( y in ProperPrefixes v or ( y = v & v in ProperPrefixes (v ^ <*x*>) ) ) by A3, TARSKI:def 1, TREES_1:def 2;
hence y in ProperPrefixes (v ^ <*x*>) by A4; :: thesis: verum