let v, w be VECTOR of Linear_Space_of_RealSequences; :: thesis: v + w = (seq_id v) + (seq_id w)
reconsider v1 = v, w1 = w as Element of Funcs (NAT,REAL) ;
(RealFuncAdd NAT) . (v1,w1) = (seq_id v) + (seq_id w)

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((RealFuncAdd NAT) . (v1,w1)) . n = ((seq_id v) + (seq_id w)) . n
thus ((RealFuncAdd NAT) . (v1,w1)) . n = (v1 . n) + (w1 . n) by FUNCSDOM: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