let X be TopStruct ; :: thesis: 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
let Y be non empty TopStruct ; :: thesis: for Z being non empty SubSpace of Y
for f being Function of X,Z holds f is Function of X,Y
let Z be non empty SubSpace of Y; :: thesis: for f being Function of X,Z holds f is Function of X,Y
let f be Function of X,Z; :: thesis: f is Function of X,Y
the carrier of Z is Subset of Y by TSEP_1:1;
then A1: rng f c= the carrier of Y by XBOOLE_1:1;
dom f = the carrier of X by FUNCT_2:def 1;
hence f is Function of X,Y by A1, FUNCT_2:2; :: thesis: verum