F + G is Function of the carrier of T, REAL ;
hence F + G is RealMap of T ; :: thesis: verum