ContMaps S,T is non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def3, Th35;
hence ContMaps S,T is complete by YELLOW_2:33; :: thesis: verum