A1: for x being set st x is Element of Complex_l2_Space holds
( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable )
proof
let x be set ; :: thesis: ( x is Element of Complex_l2_Space implies ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) )
A2: |.(seq_id x).| = |.((seq_id x) *').| by Lm18;
assume A3: x is Element of Complex_l2_Space ; :: thesis: ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable )
then x in the_set_of_ComplexSequences by CSSPACE:def 11;
hence x is Complex_Sequence by FUNCT_2:66; :: thesis: (seq_id x) (#) ((seq_id x) *') is absolutely_summable
|.(seq_id x).| (#) |.(seq_id x).| is summable by A3, Lm16;
then |.((seq_id x) (#) ((seq_id x) *')).| is summable by A2, COMSEQ_1:46;
hence (seq_id x) (#) ((seq_id x) *') is absolutely_summable by COMSEQ_3:def 9; :: thesis: verum
end;
for x being set st x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable holds
x is Element of Complex_l2_Space
proof
let x be set ; :: thesis: ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable implies x is Element of Complex_l2_Space )
assume that
A4: x is Complex_Sequence and
A5: (seq_id x) (#) ((seq_id x) *') is absolutely_summable ; :: thesis: x is Element of Complex_l2_Space
|.((seq_id x) (#) ((seq_id x) *')).| is summable by A5;
then |.(seq_id x).| (#) |.((seq_id x) *').| is summable by COMSEQ_1:46;
then A6: |.(seq_id x).| (#) |.(seq_id x).| is summable by Lm18;
x in the_set_of_ComplexSequences by A4, FUNCT_2:8;
hence x is Element of Complex_l2_Space by A6, 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 absolutely_summable ) ) by A1; :: thesis: verum