let u be VECTOR of Complex_l2_Space; :: thesis: u = seq_id u
u is VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13, CSSPACE:def 18;
hence u = seq_id u by CSSPACE:15; :: thesis: verum