let X, Y, Z be set ; 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 ; 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; ( 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
; f | Y is Function of Y,Z
dom f = X
by Def1;
then A3:
dom (f | Y) = Y
by A1, RELAT_1:62;
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; verum