let a be Real; :: thesis: for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); :: thesis: a * (v + w) = (a * v) + (a * w)
A1: a * (v + w) = a (#) (seq_id (v + w)) by Th5
.= a (#) (seq_id ((seq_id v) + (seq_id w))) by Def4
.= a (#) ((seq_id v) + (seq_id w)) by Th3
.= (a (#) (seq_id v)) + (a (#) (seq_id w)) by SEQ_1:30 ;
(a * v) + (a * w) = (seq_id (a * v)) + (seq_id (a * w)) by Def4
.= (seq_id (a (#) (seq_id v))) + (seq_id (a * w)) by Th5
.= (seq_id (a (#) (seq_id v))) + (seq_id (a (#) (seq_id w))) by Th5
.= (a (#) (seq_id v)) + (seq_id (a (#) (seq_id w))) by Th3
.= (a (#) (seq_id v)) + (a (#) (seq_id w)) by Th3 ;
hence a * (v + w) = (a * v) + (a * w) by A1; :: thesis: verum