suppose not k in dom (0 (#) f) ; :: thesis:

hence (0 (#) f) . k = 0 by FUNCT_1:def 2; :: thesis:

end;

suppose k in dom (0 (#) f) ; :: thesis:

then (0 (#) f) . k = 0 * (f . k) by VALUED_1:def 5;
hence (0 (#) f) . k = 0 ; :: thesis:

end;

end;