let m1, m2 be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( ( for t being Point of (TOP-REAL 2) holds m1 . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) & ( for t being Point of (TOP-REAL 2) holds m2 . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) implies m1 = m2 )
assume that
A4: for t being Point of (TOP-REAL 2) holds m1 . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| and
A5: for t being Point of (TOP-REAL 2) holds m2 . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ; :: thesis: m1 = m2
for x being Point of (TOP-REAL 2) holds m1 . x = m2 . x

proof

let t be Point of (TOP-REAL 2); :: thesis: m1 . t = m2 . t
thus m1 . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| by A4
.= m2 . t by A5 ; :: thesis: verum

end;

hence m1 = m2 by FUNCT_2:63; :: thesis: verum