let f1, f2 be Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL; ( ( 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))
; 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:];
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:1;
consider y1 being
Element of
X,
y2 being
Element of
Y such that A5:
y = [y1,y2]
by DOMAIN_1:1;
thus f1 . (
x,
y) =
sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))
by A2, A4, A5
.=
f2 . (
x,
y)
by A3, A4, A5
;
verum
end;
hence
f1 = f2
by BINOP_1:2; verum