let m, n be Element of NAT ; :: thesis: for IT being Function of (REAL m),(REAL n) st IT is additive holds
IT . (0* m) = 0* n
let IT be Function of (REAL m),(REAL n); :: thesis: ( IT is additive implies IT . (0* m) = 0* n )
assume AS: IT is additive ; :: thesis: IT . (0* m) = 0* n
IT . (0* m) = IT . ((0* m) + (0* m)) by RVSUM_1:33;
then IT . (0* m) = (IT . (0* m)) + (IT . (0* m)) by AS, LOPBDef5;
then 0* n = ((IT . (0* m)) + (IT . (0* m))) - (IT . (0* m)) by RVSUM_1:58;
hence 0* n = IT . (0* m) by RVSUM_1:63; :: thesis: verum