let f1, f2 be Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL ; :: thesis: ( ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) & ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f2 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) implies f1 = f2 )
assume that
A3: for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) and
A4: for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f2 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ; :: thesis: f1 = f2
for x, y being Element of [:REAL ,REAL ,REAL :] holds f1 . x,y = f2 . x,y

proof

let x, y be Element of [:REAL ,REAL ,REAL :]; :: thesis: f1 . x,y = f2 . x,y
consider x1, x2, x3 being Element of REAL such that
A5: x = [x1,x2,x3] by DOMAIN_1:15;
consider y1, y2, y3 being Element of REAL such that
A6: y = [y1,y2,y3] by DOMAIN_1:15;
thus f1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) by A3, A5, A6
.= f2 . x,y by A4, A5, A6 ; :: thesis: verum

end;

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