let f be Function; :: thesis: for X being set st X c= dom f & X <> {} holds
rng (f | X) <> {}
let X be set ; :: thesis: ( X c= dom f & X <> {} implies rng (f | X) <> {} )
assume A0: X c= dom f ; :: thesis: ( not X <> {} or rng (f | X) <> {} )
assume A1: X <> {} ; :: thesis: rng (f | X) <> {}
consider x being Element of X;
x in X by A1;
hence rng (f | X) <> {} by A0, FUNCT_1:73; :: thesis: verum