let n, m be Nat; :: thesis: #Z (n + m) = (#Z n) (#) (#Z m)

now :: thesis: for r being Real holds (#Z (n + m)) . r = ((#Z n) (#) (#Z m)) . r

let r be Real; :: thesis: (#Z (n + m)) . r = ((#Z n) (#) (#Z m)) . r
thus (#Z (n + m)) . r = r #Z (n + m) by TAYLOR_1:def 1
.= (r #Z n) * (r #Z m) by TAYLOR_1:1
.= ((#Z n) . r) * (r #Z m) by TAYLOR_1:def 1
.= ((#Z n) . r) * ((#Z m) . r) by TAYLOR_1:def 1
.= ((#Z n) (#) (#Z m)) . r by VALUED_1:5 ; :: thesis: verum

end;

hence #Z (n + m) = (#Z n) (#) (#Z m) ; :: thesis: verum