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