let v be VECTOR of ; :: thesis: 1r * v = v
1r * v = 1r (#) (seq_id v) by Th5
.= seq_id v by COMSEQ_1:24 ;
hence 1r * v = v by Def2; :: thesis: verum