let B be Polish-arity-function; :: thesis: ( B is empty-yielding iff for a being object st a in dom B holds
B . a = 0 )
thus ( B is empty-yielding implies for a being object st a in dom B holds
B . a = 0 ) ; :: thesis: ( ( for a being object st a in dom B holds
B . a = 0 ) implies B is empty-yielding )
assume A1: for a being object st a in dom B holds
B . a = 0 ; :: thesis: B is empty-yielding
for a being object st a in dom B holds
B . a is empty

proof

let a be object ; :: thesis: ( a in dom B implies B . a is empty )
assume a in dom B ; :: thesis: B . a is empty
then B . a = {} by A1;
hence B . a is empty ; :: thesis: verum

end;

hence B is empty-yielding by FUNCT_1:def 8; :: thesis: verum