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),(+ x2,y2)*] ) & ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c2 = [*(+ x1,y1),(+ x2,y2)*] ) implies c1 = c2 )
given x1, x2, y1, y2 being Element of REAL such that A5: x = [*x1,x2*] and
A6: y = [*y1,y2*] and
A7: c1 = [*(+ x1,y1),(+ x2,y2)*] ; :: 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),(+ x2,y2)*] ) or c1 = c2 )
given x19, x29, y19, y29 being Element of REAL such that A8: x = [*x19,x29*] and
A9: y = [*y19,y29*] and
A10: c2 = [*(+ x19,y19),(+ x29,y29)*] ; :: thesis: c1 = c2
A11: ( x1 = x19 & x2 = x29 ) by A5, A8, ARYTM_0:12;
A12: y1 = y19 by A6, A9, ARYTM_0:12;
thus c1 = c2 by A6, A7, A9, A10, A11, A12, ARYTM_0:12; :: thesis: verum