let S, T, X, Y be non empty TopSpace; ( 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 #)
; ( 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
; WAYBEL25:def 1 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
; WAYBEL25:def 1 ex r being continuous Function of Y,T st r * cc = id T
take
rr
; rr * cc = id T
thus
rr * cc = id T
by A1, A3; verum