let u be VECTOR of ; :: thesis: u = seq_id u
u is VECTOR of by CLVECT_1:30, CSSPACE:15, CSSPACE:def 20;
hence u = seq_id u by CSSPACE:17; :: thesis: verum