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 FUNCT_2:8, FUNCT_2:66;
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; :: 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