let x, y be set ; :: thesis: ( <*x*> is_a_prefix_of <*y*> implies x = y )
assume A1: <*x*> is_a_prefix_of <*y*> ; :: thesis: x = y
( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:40;
then A2: <*x*> = <*y*> by A1, CARD_2:102;
<*x*> . 1 = x by FINSEQ_1:40;
hence x = y by A2, FINSEQ_1:40; :: thesis: verum