let it1, it2 be RealMap of (TOP-REAL 2); :: thesis: ( ( for p being Point of (TOP-REAL 2) holds it1 . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds it2 . p = p `2 ) implies it1 = it2 )
assume that
A5: for p being Point of (TOP-REAL 2) holds it1 . p = p `2 and
A6: for p being Point of (TOP-REAL 2) holds it2 . p = p `2 ; :: thesis: it1 = it2

now :: thesis: for p being Point of (TOP-REAL 2) holds it1 . p = it2 . p

let p be Point of (TOP-REAL 2); :: thesis: it1 . p = it2 . p
thus it1 . p = p `2 by A5
.= it2 . p by A6 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:63; :: thesis: verum