let n, m be 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 A1: IT is additive ; :: thesis: IT . (0* m) = 0* n
IT . (0* m) = IT . ((0* m) + (0* m)) by RVSUM_1:16;
then IT . (0* m) = (IT . (0* m)) + (IT . (0* m)) by A1;
then 0* n = ((IT . (0* m)) + (IT . (0* m))) - (IT . (0* m)) by RVSUM_1:37;
hence 0* n = IT . (0* m) by RVSUM_1:42; :: thesis: verum