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

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

hence
f1 = f2
by FUNCT_2:63; :: thesis: verum
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;thus f1 . q = |(p,q)| by A6

.= f2 . q by A7 ; :: thesis: verum