let f, g be Function of [:(REAL n),(REAL n):],REAL; :: thesis: ( ( for x, y being Element of REAL n holds f . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds g . (x,y) = |.(x - y).| ) implies f = g )
assume that
A2: for x, y being Element of REAL n holds f . (x,y) = |.(x - y).| and
A3: for x, y being Element of REAL n holds g . (x,y) = |.(x - y).| ; :: thesis: f = g
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider f = f, g = g as Function of [:(REAL n),(REAL n):],REAL ;

now :: thesis: for x, y being Element of REAL n holds f . (x,y) = g . (x,y)

let x, y be Element of REAL n; :: thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = |.(x - y).| by A2
.= g . (x,y) by A3 ; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum