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 A3: x = [*x1,x2*] and
A4: y = [*y1,y2*] and
A5: 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 A6: x = [*x1',x2'*] and
A7: y = [*y1',y2'*] and
A8: c2 = [*(+ x1',y1'),(+ x2',y2')*] ; :: thesis: c1 = c2
( x1 = x1' & x2 = x2' & y1 = y1' & y2 = y2' ) by A3, A4, A6, A7, ARYTM_0:12;
hence c1 = c2 by A5, A8; :: thesis: verum