let S, T, X, Y be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) & S is_Retract_of X implies T is_Retract_of Y )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) ; :: thesis: ( not S is_Retract_of X or T is_Retract_of Y )
given c being continuous Function of S,X, r being continuous Function of X,S such that A3: r * c = id S ; :: according to WAYBEL25:def 1 :: thesis: T is_Retract_of Y
reconsider rr = r as continuous Function of Y,T by A1, A2, YELLOW12:36;
reconsider cc = c as continuous Function of T,Y by A1, A2, YELLOW12:36;
take cc ; :: according to WAYBEL25:def 1 :: thesis: ex r being continuous Function of Y,T st r * cc = id T
take rr ; :: thesis: rr * cc = id T
thus rr * cc = id T by A1, A3; :: thesis: verum