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 A1: y in ProperPrefixes (v ^ <*x*>) ; :: thesis: y in (ProperPrefixes v) \/ {v}
consider v1 being FinSequence such that
A2: y = v1 and
A3: v1 is_a_proper_prefix_of v ^ <*x*> by A1, TREES_1:def 4;
A4: ( ( v1 is_a_prefix_of v & v1 <> v ) or v1 = v ) by A3, TREES_1:32;
A5: ( v1 is_a_proper_prefix_of v or v1 in {v} ) by A4, TARSKI:def 1, XBOOLE_0:def 8;
A6: ( y in ProperPrefixes v or y in {v} ) by A2, A5, TREES_1:def 4;
thus y in (ProperPrefixes v) \/ {v} by A6, 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 A7: y in (ProperPrefixes v) \/ {v} ; :: thesis: y in ProperPrefixes (v ^ <*x*>)
A8: ( y in ProperPrefixes v or y in {v} ) by A7, XBOOLE_0:def 3;

A9: now

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

end;

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