for x being object st x in dom ((delneg f) (#) (delpos f)) holds
((delneg f) (#) (delpos f)) . x is empty
proof
let x be object ; :: thesis: ( x in dom ((delneg f) (#) (delpos f)) implies ((delneg f) (#) (delpos f)) . x is empty )
assume A1: x in dom ((delneg f) (#) (delpos f)) ; :: thesis: ((delneg f) (#) (delpos f)) . x is empty
A2: ( (delneg f) . x = 0 or (delpos f) . x = 0 ) by ZOR;
((delneg f) (#) (delpos f)) . x = ((delneg f) . x) * ((delpos f) . x) by A1, VALUED_1:def 4
.= 0 by A2 ;
hence ((delneg f) (#) (delpos f)) . x is empty by ORDINAL1:def 13; :: thesis: verum
end;
hence (delneg f) (#) (delpos f) is empty-yielding by FUNCT_1:def 8; :: thesis: verum