let f1, f2 be Function of (TOP-REAL n),R^1; :: thesis: ( ( for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ) implies f1 = f2 )
assume that
A6: for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| and
A7: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ; :: thesis: f1 = f2
for q being Point of (TOP-REAL n) holds f1 . q = f2 . q

proof

let q be Point of (TOP-REAL n); :: thesis: f1 . q = f2 . q
thus f1 . q = |(p,q)| by A6
.= f2 . q by A7 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum