let f1, f2 be Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL; :: thesis: ( ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) implies f1 = f2 )
assume that
A2: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) and
A3: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f2 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ; :: thesis: f1 = f2
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] 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:]; :: thesis: f1 . (x,y) = f2 . (x,y)
consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z such that
A4: x = [x1,x2,x3] by DOMAIN_1:3;
consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z such that
A5: y = [y1,y2,y3] by DOMAIN_1:3;
thus f1 . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) by A2, A4, A5
.= f2 . (x,y) by A3, A4, A5 ; :: thesis: verum

end;

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