let c1, c2 be number ; :: thesis: ( ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) & ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) implies c1 = c2 )
given x1, x2, y1, y2 being Element of REAL such that A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: c1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ; :: thesis: ( for x1, x2, y1, y2 being Element of REAL holds
( not x = [*x1,x2*] or not y = [*y1,y2*] or not c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) or c1 = c2 )
given x19, x29, y19, y29 being Element of REAL such that A13: x = [*x19,x29*] and
A14: y = [*y19,y29*] and
A15: c2 = [*(+ ((* (x19,y19)),(opp (* (x29,y29))))),(+ ((* (x19,y29)),(* (x29,y19))))*] ; :: thesis: c1 = c2
A16: ( x1 = x19 & x2 = x29 ) by A10, A13, ARYTM_0:10;
( y1 = y19 & y2 = y29 ) by A11, A14, ARYTM_0:10;
hence c1 = c2 by A12, A15, A16; :: thesis: verum