for x being set st x in rng ((0,0) Subnomial n) holds
x = {}
proof
let x be set ; :: thesis: ( x in rng ((0,0) Subnomial n) implies x = {} )
assume x in rng ((0,0) Subnomial n) ; :: thesis: x = {}
then ex k being object st
( k in dom ((0,0) Subnomial n) & ((0,0) Subnomial n) . k = x ) by FUNCT_1:def 3;
hence x = {} ; :: thesis: verum
end;
hence (0,0) Subnomial n is empty-yielding by RELAT_1:149; :: thesis: verum