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 ) )

( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ; :: thesis: verum

( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )

proof

hence
for x being set holds
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;( 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

( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ; :: thesis: verum