for X being TopStruct
for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y