let X, Y, Z be set ; :: thesis: for f being Function of X,Y st X c= Z holds
f | Z = f
let f be Function of X,Y; :: thesis: ( X c= Z implies f | Z = f )

per cases not ( Y = {} & not X = {} & not ( Y = {} & X <> {} ) ) ;

suppose ( Y = {} implies X = {} ) ; :: thesis: ( X c= Z implies f | Z = f )

then dom f = X by Def1;
hence ( X c= Z implies f | Z = f ) by RELAT_1:97; :: thesis: verum

end;

suppose ( Y = {} & X <> {} ) ; :: thesis: ( X c= Z implies f | Z = f )

hence ( X c= Z implies f | Z = f ) ; :: thesis: verum

end;

end;