let v, w be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: v + w = (seq_id v) + (seq_id w)
reconsider v1 = v, w1 = w as Element of Funcs (NAT,COMPLEX) ;
reconsider f = (ComplexFuncAdd NAT) . (v1,w1) as Function of NAT,COMPLEX by FUNCT_2:66;
f = (seq_id v) + (seq_id w)

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: f . n = ((seq_id v) + (seq_id w)) . n
thus f . n = (v1 . n) + (w1 . n) by CFUNCDOM:1
.= ((seq_id v) + (seq_id w)) . n by VALUED_1:1 ; :: thesis: verum

end;

hence v + w = (seq_id v) + (seq_id w) ; :: thesis: verum