let m be Nat; :: thesis: (0* m) + (0* m) = 0* m
A1: dom (0* m) = Seg m by FUNCOP_1:13;
( dom addreal = [:REAL,REAL:] & rng (0* m) c= REAL ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then A2: [:(rng (0* m)),(rng (0* m)):] c= dom addreal by ZFMISC_1:96;
A3: dom ((0* m) + (0* m)) = dom (addreal .: ((0* m),(0* m))) by RVSUM_1:def 4
.= (dom (0* m)) /\ (dom (0* m)) by A2, FUNCOP_1:69
.= Seg m by FUNCOP_1:13 ;
for k being Nat st k in dom (0* m) holds
(0* m) . k = ((0* m) + (0* m)) . k

proof

let k be Nat; :: thesis: ( k in dom (0* m) implies (0* m) . k = ((0* m) + (0* m)) . k )
assume A4: k in dom (0* m) ; :: thesis: (0* m) . k = ((0* m) + (0* m)) . k
(0* m) . k = 0 ;
then ((0* m) + (0* m)) . k = 0 + 0 by A3, A1, A4, VALUED_1:def 1;
hence (0* m) . k = ((0* m) + (0* m)) . k ; :: thesis: verum

end;

hence (0* m) + (0* m) = 0* m by A3, FINSEQ_1:13, FUNCOP_1:13; :: thesis: verum