let c1, c2 be number ; ( 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))*]
; ( 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 A6:
x = [*x19,x29*]
and
A7:
y = [*y19,y29*]
and
A8:
c2 = [*(+ (x19,y19)),(+ (x29,y29))*]
; c1 = c2
A9:
( x1 = x19 & x2 = x29 )
by A3, A6, ARYTM_0:10;
y1 = y19
by A4, A7, ARYTM_0:10;
hence
c1 = c2
by A4, A5, A7, A8, A9, ARYTM_0:10; verum