let X be non empty TopSpace; :: thesis: for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
let Y, Z be monotone-convergence T_0-TopSpace; :: thesis: ( Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous implies ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
assume Y is_Retract_of Z ; :: thesis: ( not oContMaps (X,Z) is complete or not oContMaps (X,Z) is continuous or ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
then consider S being non empty SubSpace of Z such that
A1: S is_a_retract_of Z and
A2: S,Y are_homeomorphic by YELLOW16:57;
assume ( oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous ) ; :: thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
then A3: ( oContMaps (X,S) is complete & oContMaps (X,S) is continuous ) by A1, Th22;
oContMaps (X,S), oContMaps (X,Y) are_isomorphic by A2, Th21;
hence ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A3, WAYBEL15:9, WAYBEL20:18; :: thesis: verum