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 A9: x = [*x1,x2*] and
A10: y = [*y1,y2*] and
A11: 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 x1', x2', y1', y2' being Element of REAL such that A12: x = [*x1',x2'*] and
A13: y = [*y1',y2'*] and
A14: c2 = [*(+ (* x1',y1'),(opp (* x2',y2'))),(+ (* x1',y2'),(* x2',y1'))*] ; :: thesis: c1 = c2
( x1 = x1' & x2 = x2' & y1 = y1' & y2 = y2' ) by A9, A10, A12, A13, ARYTM_0:12;
hence c1 = c2 by A11, A14; :: thesis: verum