for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )

proof

let x be set ; :: thesis: ( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by CSSPACE:def 1;
hence ( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) by CSSPACE:def 11, CSSPACE:def 18; :: thesis: verum

end;

hence for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ; :: thesis: verum