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 A1: X c= dom f ; :: thesis: ( not X <> {} or rng (f | X) <> {} )
set x = the Element of X;
assume X <> {} ; :: thesis: rng (f | X) <> {}
then the Element of X in X ;
hence rng (f | X) <> {} by A1, FUNCT_1:50; :: thesis: verum