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