let X, Y, Z be set ; :: thesis: for D being non empty set
for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z
let D be non empty set ; :: thesis: for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z
let f be Function of X,D; :: thesis: ( Y c= X & f .: Y c= Z implies f | Y is Function of Y,Z )
assume that
A1: Y c= X and
A2: f .: Y c= Z ; :: thesis: f | Y is Function of Y,Z
dom f = X by Def1;
then A3: dom (f | Y) = Y by A1, RELAT_1:62;

A4: now :: thesis: ( Z = {} implies Y = {} )

assume Z = {} ; :: thesis: Y = {}
then rng (f | Y) = {} by A2, RELAT_1:115;
hence Y = {} by A3, RELAT_1:42; :: thesis: verum

end;

rng (f | Y) c= Z by A2, RELAT_1:115;
hence f | Y is Function of Y,Z by A3, A4, Def1, RELSET_1:4; :: thesis: verum