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

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 by FUNCT_2:113; :: thesis: verum