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 set ; :: 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
A2: y = v1 and
A3: v1 is_a_proper_prefix_of v ^ <*x*> by TREES_1:def 4;
( ( v1 is_a_prefix_of v & v1 <> v ) or v1 = v ) by A3, TREES_1:32;
then ( v1 is_a_proper_prefix_of v or v1 in {v} ) by TARSKI:def 1, XBOOLE_0:def 8;
then ( y in ProperPrefixes v or y in {v} ) by A2, TREES_1:def 4;
hence y in (ProperPrefixes v) \/ {v} by XBOOLE_0:def 3; :: thesis: verum

end;

let y be set ; :: 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 A8: ( y in ProperPrefixes v or y in {v} ) by XBOOLE_0:def 3;

A9: now

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

end;

v ^ {} = v by FINSEQ_1:47;
then ( v is_a_prefix_of v ^ <*x*> & v <> v ^ <*x*> ) by FINSEQ_1:46, TREES_1:8;
then v is_a_proper_prefix_of v ^ <*x*> by XBOOLE_0:def 8;
then ( y in ProperPrefixes v or ( y = v & v in ProperPrefixes (v ^ <*x*>) ) ) by A8, TARSKI:def 1, TREES_1:def 4;
hence y in ProperPrefixes (v ^ <*x*>) by A9; :: thesis: verum