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 * (b * v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #); :: thesis: (a * b) * v = a * (b * v)
(a * b) * v = (a * b) (#) (seq_id v) by Th5
.= a (#) (b (#) (seq_id v)) by SEQ_1:31
.= a (#) (seq_id (b (#) (seq_id v))) by Th3
.= a (#) (seq_id (b * v)) by Th5 ;
hence (a * b) * v = a * (b * v) by Th5; :: thesis: verum