let f, g be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( ( for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ) implies f = g )
assume that
A2: for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| and
A3: for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| ; :: thesis: f = g

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

let p be Point of (TOP-REAL 2); :: thesis: f . p = g . p
thus f . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| by A2
.= g . p by A3 ; :: thesis: verum

end;

hence f = g ; :: thesis: verum