let X be TopStruct ; :: thesis: 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
let Y be non empty TopStruct ; :: thesis: for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
let f be Function of X,Y; :: thesis: for P being Subset of X holds f | P is Function of (X | P),Y
let P be Subset of X; :: thesis: f | P is Function of (X | P),Y
P = the carrier of (X | P) by Th8;
hence f | P is Function of (X | P),Y by FUNCT_2:32; :: thesis: verum