per cases ( not k in dom (0 (#) f) or k in dom (0 (#) f) ) ;

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

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

end;

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

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

end;

end;