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