for X being TopStruct
for Y being non empty TopStruct
for K0 being Subset of X
for f being Function of X,Y
for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous