deffunc H₁( Point of (TOP-REAL 2)) -> Element of the carrier of (TOP-REAL 2) = |[(Re (Rotate ((($1 `1) + (($1 `2) * <i>)),a))),(Im (Rotate ((($1 `1) + (($1 `2) * <i>)),a)))]|;
consider f being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A1: for p being Point of (TOP-REAL 2) holds f . p = H₁(p) from FUNCT_2:sch 4();
take f ; :: 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)))]|
thus 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)))]| by A1; :: thesis: verum