let a, b be Real; :: thesis: for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); :: thesis: (a + b) * v = (a * v) + (b * v)
for s being set st s in NAT holds
((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s

proof

let s be set ; :: thesis: ( s in NAT implies ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s )
assume A1: s in NAT ; :: thesis: ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s
((a + b) (#) (seq_id v)) . s = (a + b) * ((seq_id v) . s) by A1, SEQ_1:9
.= (a * ((seq_id v) . s)) + (b * ((seq_id v) . s))
.= ((a (#) (seq_id v)) . s) + (b * ((seq_id v) . s)) by A1, SEQ_1:9
.= ((a (#) (seq_id v)) . s) + ((b (#) (seq_id v)) . s) by A1, SEQ_1:9 ;
hence ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s by A1, SEQ_1:7; :: thesis: verum

end;

then A2: (a + b) (#) (seq_id v) = (a (#) (seq_id v)) + (b (#) (seq_id v)) by FUNCT_2:12;
(a * v) + (b * v) = (seq_id (a * v)) + (seq_id (b * v)) by Def4
.= (seq_id (a (#) (seq_id v))) + (seq_id (b * v)) by Th5
.= (seq_id (a (#) (seq_id v))) + (seq_id (b (#) (seq_id v))) by Th5
.= (a (#) (seq_id v)) + (seq_id (b (#) (seq_id v))) by Th3
.= (a (#) (seq_id v)) + (b (#) (seq_id v)) by Th3 ;
hence (a + b) * v = (a * v) + (b * v) by A2, Th5; :: thesis: verum