min ((n + 0),(n + m)) = n by XREAL_1:6, XXREAL_0:def 9;
then reconsider h = f + g as n -element complex-valued FinSequence ;
( len f = n & len h = n ) by FINSEQ_3:153;
then A1: dom f = dom h by FINSEQ_3:29;
for c being Nat st c in dom (f + g) holds
(f + g) . c = f . c

proof

let c be Nat; :: thesis: ( c in dom (f + g) implies (f + g) . c = f . c )
assume B1: c in dom (f + g) ; :: thesis: (f + g) . c = f . c
reconsider f = f as complex-valued Function ;
reconsider g = g as complex-valued Function ;
reconsider c = c as object ;
(f + g) . c = (f . c) + (g . c) by VALUED_1:def 1, B1
.= (f . c) + 0 ;
hence (f + g) . c = f . c ; :: thesis: verum

end;

hence f + g = f by A1, FINSEQ_1:13; :: thesis: verum