let x1, x2, y1, y2 be Element of REAL ; :: thesis: ( [*x1,x2*] = [*y1,y2*] implies ( x1 = y1 & x2 = y2 ) )
assume A1: [*x1,x2*] = [*y1,y2*] ; :: thesis: ( x1 = y1 & x2 = y2 )

per cases ( x2 = 0 or x2 <> 0 ) ;

suppose A2: x2 = 0 ; :: thesis: ( x1 = y1 & x2 = y2 )

then A3: [*x1,x2*] = x1 by Def7;

A4: now

assume y2 <> 0 ; :: thesis: contradiction
then x1 = 0 ,1 --> y1,y2 by A1, A3, Def7;
hence contradiction by Th10; :: thesis: verum

end;

hence x1 = y1 by A1, A3, Def7; :: thesis: x2 = y2
thus x2 = y2 by A2, A4; :: thesis: verum

end;

suppose x2 <> 0 ; :: thesis: ( x1 = y1 & x2 = y2 )

then A5: [*y1,y2*] = 0 ,1 --> x1,x2 by A1, Def7;

now

assume y2 = 0 ; :: thesis: contradiction
then [*y1,y2*] = y1 by Def7;
hence contradiction by A5, Th10; :: thesis: verum

end;

then [*y1,y2*] = 0 ,1 --> y1,y2 by Def7;
hence ( x1 = y1 & x2 = y2 ) by A5, FUNCT_4:72; :: thesis: verum

end;

end;