theorem :: TOPREALA:7

for X being TopStruct
for Y being non empty TopStruct
for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y