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;