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 Def5;

A4: now :: thesis: not y2 <> 0

assume y2 <> 0 ; :: thesis: contradiction
then x1 = (0,1) --> (y1,y2) by A1, A3, Def5;
hence contradiction by Th8; :: thesis: verum

end;

hence x1 = y1 by A1, A3, Def5; :: 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, Def5;

now :: thesis: not y2 = 0

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

end;

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

end;

end;