let x, y be set ; :: thesis: ( <*x*> is_a_prefix_of <*y*> iff x = y )
thus ( <*x*> is_a_prefix_of <*y*> implies x = y ) :: thesis: ( x = y implies <*x*> is_a_prefix_of <*y*> )

proof

assume A1: <*x*> is_a_prefix_of <*y*> ; :: thesis: x = y
( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:57;
then ( <*x*> = <*y*> & <*x*> . 1 = x & <*y*> . 1 = y ) by A1, Th15, FINSEQ_1:57;
hence x = y ; :: thesis: verum

end;

thus ( x = y implies <*x*> is_a_prefix_of <*y*> ) ; :: thesis: verum