let f1, f2 be Function of [:[:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:],[:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:]:],REAL ; :: thesis: ( ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f1 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f2 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) ) implies f1 = f2 )
assume that
A3: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f1 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) and
A4: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f2 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) ; :: thesis: f1 = f2
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] holds f1 . x,y = f2 . x,y

proof

let x, y be Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:]; :: thesis: f1 . x,y = f2 . x,y
consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z, x4 being Element of W such that
A5: x = [x1,x2,x3,x4] by DOMAIN_1:31;
consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z, y4 being Element of W such that
A6: y = [y1,y2,y3,y4] by DOMAIN_1:31;
thus f1 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) by A3, A5, A6
.= f2 . x,y by A4, A5, A6 ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum