let X be non empty TopSpace; :: thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_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 Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z st Y is_a_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 be non empty SubSpace of Z; :: thesis: ( Y is_a_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_a_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 A1: oContMaps (X,Y) is_a_retract_of oContMaps (X,Z) by Th20;
assume ( oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous ) ; :: thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
hence ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A1, YELLOW16:21, YELLOW16:22; :: thesis: verum