let f1, f2 be Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:],REAL ; :: thesis: ( ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
f1 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
f2 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) implies f1 = f2 )
assume that
A2: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
f1 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) and
A3: for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
f2 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ; :: thesis: f1 = f2
for x, y being Element of [:the carrier of X,the carrier of Y:] holds f1 . x,y = f2 . x,y

proof

let x, y be Element of [:the carrier of X,the carrier of Y:]; :: thesis: f1 . x,y = f2 . x,y
consider x1 being Element of X, x2 being Element of Y such that
A4: x = [x1,x2] by DOMAIN_1:9;
consider y1 being Element of X, y2 being Element of Y such that
A5: y = [y1,y2] by DOMAIN_1:9;
thus f1 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) by A2, A4, A5
.= f2 . x,y by A3, A4, A5 ; :: thesis: verum

end;

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