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