let f1, f2 be Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL; :: thesis: ( ( for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) & ( for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) implies f1 = f2 )

assume that

A2: for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) and

A3: for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ; :: thesis: f1 = f2

for x, y being Element of [:REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) & ( for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) implies f1 = f2 )

assume that

A2: for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) and

A3: for x1, y1, x2, y2 being Element of REAL

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

f2 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ; :: thesis: f1 = f2

for x, y being Element of [:REAL,REAL:] holds f1 . (x,y) = f2 . (x,y)

proof

hence
f1 = f2
by BINOP_1:2; :: thesis: verum
let x, y be Element of [:REAL,REAL:]; :: thesis: f1 . (x,y) = f2 . (x,y)

consider x1, x2 being Element of REAL such that

A4: x = [x1,x2] by DOMAIN_1:1;

consider y1, y2 being Element of REAL such that

A5: y = [y1,y2] by DOMAIN_1:1;

thus f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by A2, A4, A5

.= f2 . (x,y) by A3, A4, A5 ; :: thesis: verum

end;consider x1, x2 being Element of REAL such that

A4: x = [x1,x2] by DOMAIN_1:1;

consider y1, y2 being Element of REAL such that

A5: y = [y1,y2] by DOMAIN_1:1;

thus f1 . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) by A2, A4, A5

.= f2 . (x,y) by A3, A4, A5 ; :: thesis: verum