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