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

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