let f be real-valued Function; :: thesis: for x being object holds
( (delneg f) . x = 0 or (delpos f) . x = 0 )
let x be object ; :: thesis: ( (delneg f) . x = 0 or (delpos f) . x = 0 )
B2: f . x = ((delneg f) . x) - ((delpos f) . x) by VAL;
( f . x = (delneg f) . x or f . x = - ((delpos f) . x) ) by VOR;
hence ( (delneg f) . x = 0 or (delpos f) . x = 0 ) by B2; :: thesis: verum