for T being non empty TopSpace
for S being non empty SubSpace of T
for f being Function of T,S st f is being_a_retraction holds
rng f = the carrier of S