let it1, it2 be RealMap of (TOP-REAL 2); :: thesis: ( ( for p being Point of (TOP-REAL 2) holds it1 . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds it2 . p = p `1 ) implies it1 = it2 )
assume that
A2: for p being Point of (TOP-REAL 2) holds it1 . p = p `1 and
A3: for p being Point of (TOP-REAL 2) holds it2 . p = p `1 ; :: 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 `1 by A2
.= it2 . p by A3 ; :: thesis: verum

end;

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