let x, y, z be Point of Complex_l2_Space ; :: thesis: for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Complex; :: thesis: ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
set seqx = seq_id x;
A1: x .|. x = the scalar of Complex_l2_Space . x,x by CSSPACE:def 12
.= Sum ((seq_id x) (#) ((seq_id x) *' )) by CSSPACE:def 19, CSSPACE:def 20 ;
A2: (seq_id x) (#) ((seq_id x) *' ) is absolutely_summable by Lm20;
then Sum ((seq_id x) (#) ((seq_id x) *' )) = (Sum (Re ((seq_id x) (#) ((seq_id x) *' )))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *' )))) * <i> ) by COMSEQ_3:54;
then A3: ( Re (x .|. x) = Sum (Re ((seq_id x) (#) ((seq_id x) *' ))) & Im (x .|. x) = Sum (Im ((seq_id x) (#) ((seq_id x) *' ))) ) by A1, COMPLEX1:28;

A4: now

set seq = seq_id x;
A5: x .|. x = the scalar of Complex_l2_Space . x,x by CSSPACE:def 12
.= Sum ((seq_id x) (#) ((seq_id x) *' )) by CSSPACE:def 19, CSSPACE:def 20 ;
set rseq = Re ((seq_id x) (#) ((seq_id x) *' ));
A6: for n being Element of NAT holds (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 )

proof

let n be Element of NAT ; :: thesis: (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 )
(Re ((seq_id x) (#) ((seq_id x) *' ))) . n = (((Re (seq_id x)) (#) (Re ((seq_id x) *' ))) - ((Im (seq_id x)) (#) (Im ((seq_id x) *' )))) . n by COMSEQ_3:21
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *' ))) . n) + ((- ((Im (seq_id x)) (#) (Im ((seq_id x) *' )))) . n) by SEQ_1:11
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *' ))) . n) + (- (((Im (seq_id x)) (#) (Im ((seq_id x) *' ))) . n)) by SEQ_1:14
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *' ))) . n) - (((Im (seq_id x)) (#) (Im ((seq_id x) *' ))) . n)
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *' )) . n)) - (((Im (seq_id x)) (#) (Im ((seq_id x) *' ))) . n) by SEQ_1:12
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *' )) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *' )) . n)) by SEQ_1:12
.= ((Re ((seq_id x) . n)) * ((Re ((seq_id x) *' )) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *' )) . n)) by COMSEQ_3:def 5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *' )) . n)) by COMSEQ_3:def 5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - ((Im ((seq_id x) . n)) * ((Im ((seq_id x) *' )) . n)) by COMSEQ_3:def 6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *' ) . n))) by COMSEQ_3:def 6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *' ))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *' ) . n))) by COMSEQ_2:def 2
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *' ))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *' ))) by COMSEQ_2:def 2
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *' ))) by COMPLEX1:112
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (- (Im ((seq_id x) . n)))) by COMPLEX1:112
.= ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) * (Im ((seq_id x) . n))) ;
hence (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) ; :: thesis: verum

end;

A7: for n being Element of NAT holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n
A8: (Im ((seq_id x) . n)) ^2 >= 0 by XREAL_1:65;
( (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) & (Re ((seq_id x) . n)) ^2 >= 0 ) by A6, XREAL_1:65;
then (Re ((seq_id x) (#) ((seq_id x) *' ))) . n >= 0 + 0 by A8, XREAL_1:9;
hence 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n ; :: thesis: verum

end;

A9: (seq_id x) (#) ((seq_id x) *' ) is absolutely_summable by Lm20;
assume x .|. x = 0 ; :: thesis: x = 0. Complex_l2_Space
then (Sum (Re ((seq_id x) (#) ((seq_id x) *' )))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *' )))) * <i> ) = 0 by A5, A9, COMSEQ_3:54;
then A10: Sum (Re ((seq_id x) (#) ((seq_id x) *' ))) = 0 by COMPLEX1:12, COMPLEX1:28;
A11: for n being Element of NAT holds (seq_id x) . n = 0

proof

let n be Element of NAT ; :: thesis: (seq_id x) . n = 0
(Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) by A6;
then ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) = 0 by A9, A10, A7, RSSPACE:21;
hence (seq_id x) . n = 0 by COMPLEX1:13; :: thesis: verum

end;

x is Element of the_set_of_ComplexSequences by CSSPACE:def 11, CSSPACE:def 20;
hence x = 0. Complex_l2_Space by A11, Lm11, CSSPACE:def 6; :: thesis: verum

end;

A12: now

assume A13: x = 0. Complex_l2_Space ; :: thesis: x .|. x = 0
A14: for n being Element of NAT holds ((seq_id x) (#) ((seq_id x) *' )) . n = 0

proof

let n be Element of NAT ; :: thesis: ((seq_id x) (#) ((seq_id x) *' )) . n = 0
thus ((seq_id x) (#) ((seq_id x) *' )) . n = ((seq_id x) . n) * (((seq_id x) *' ) . n) by VALUED_1:5
.= 0c * (((seq_id x) *' ) . n) by A13, Lm11, CSSPACE:def 6
.= 0 ; :: thesis: verum

end;

thus x .|. x = the scalar of Complex_l2_Space . x,x by CSSPACE:def 12
.= Sum ((seq_id x) (#) ((seq_id x) *' )) by CSSPACE:def 19, CSSPACE:def 20
.= 0 by A14, CSSPACE:88 ; :: thesis: verum

end;

set seqy = seq_id y;
A15: for n being Element of NAT holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n
A16: ( (Re ((seq_id x) . n)) ^2 >= 0 & (Im ((seq_id x) . n)) ^2 >= 0 ) by XREAL_1:65;
(Re ((seq_id x) (#) ((seq_id x) *' ))) . n = Re (((seq_id x) (#) ((seq_id x) *' )) . n) by COMSEQ_3:def 5
.= Re (((seq_id x) . n) * (((seq_id x) *' ) . n)) by VALUED_1:5
.= Re (((seq_id x) . n) * (((seq_id x) . n) *' )) by COMSEQ_2:def 2
.= ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) by COMPLEX1:126 ;
then (Re ((seq_id x) (#) ((seq_id x) *' ))) . n >= 0 + 0 by A16, XREAL_1:9;
hence 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n ; :: thesis: verum

end;

|.(seq_id x).| (#) |.(seq_id y).| is summable by Lm17;
then |.((seq_id x) *' ).| (#) |.(seq_id y).| is summable by Lm19;
then |.(((seq_id x) *' ) (#) (seq_id y)).| is summable by COMSEQ_1:49;
then A17: ((seq_id x) *' ) (#) (seq_id y) is absolutely_summable by COMSEQ_3:def 13;
set seqz = seq_id z;
A18: for n being Element of NAT holds (Im ((seq_id x) (#) ((seq_id x) *' ))) . n = 0

proof

let n be Element of NAT ; :: thesis: (Im ((seq_id x) (#) ((seq_id x) *' ))) . n = 0
(Im ((seq_id x) (#) ((seq_id x) *' ))) . n = Im (((seq_id x) (#) ((seq_id x) *' )) . n) by COMSEQ_3:def 6
.= Im (((seq_id x) . n) * (((seq_id x) *' ) . n)) by VALUED_1:5
.= Im (((seq_id x) . n) * (((seq_id x) . n) *' )) by COMSEQ_2:def 2 ;
hence (Im ((seq_id x) (#) ((seq_id x) *' ))) . n = 0 by COMPLEX1:126; :: thesis: verum

end;

|.(seq_id x).| (#) |.(seq_id z).| is summable by Lm17;
then |.(seq_id x).| (#) |.((seq_id z) *' ).| is summable by Lm19;
then |.((seq_id x) (#) ((seq_id z) *' )).| is summable by COMSEQ_1:49;
then A19: (seq_id x) (#) ((seq_id z) *' ) is absolutely_summable by COMSEQ_3:def 13;
|.(seq_id y).| (#) |.(seq_id z).| is summable by Lm17;
then |.(seq_id y).| (#) |.((seq_id z) *' ).| is summable by Lm19;
then |.((seq_id y) (#) ((seq_id z) *' )).| is summable by COMSEQ_1:49;
then A20: (seq_id y) (#) ((seq_id z) *' ) is absolutely_summable by COMSEQ_3:def 13;
A21: (x + y) .|. z = the scalar of Complex_l2_Space . (x + y),z by CSSPACE:def 12
.= Sum ((seq_id (x + y)) (#) ((seq_id z) *' )) by CSSPACE:def 19, CSSPACE:def 20
.= Sum ((seq_id ((seq_id x) + (seq_id y))) (#) ((seq_id z) *' )) by Lm13
.= Sum (((seq_id x) + (seq_id y)) (#) ((seq_id z) *' )) by CSSPACE:3
.= Sum (((seq_id x) (#) ((seq_id z) *' )) + ((seq_id y) (#) ((seq_id z) *' ))) by COMSEQ_1:13
.= (Sum ((seq_id x) (#) ((seq_id z) *' ))) + (Sum ((seq_id y) (#) ((seq_id z) *' ))) by A19, A20, COMSEQ_3:55
.= (the scalar of Complex_l2_Space . x,z) + (Sum ((seq_id y) (#) ((seq_id z) *' ))) by CSSPACE:def 19, CSSPACE:def 20
.= (the scalar of Complex_l2_Space . x,z) + (the scalar of Complex_l2_Space . y,z) by CSSPACE:def 19, CSSPACE:def 20
.= (x .|. z) + (the scalar of Complex_l2_Space . y,z) by CSSPACE:def 12
.= (x .|. z) + (y .|. z) by CSSPACE:def 12 ;
|.(seq_id x).| (#) |.(seq_id y).| is summable by Lm17;
then |.(seq_id x).| (#) |.((seq_id y) *' ).| is summable by Lm19;
then |.((seq_id x) (#) ((seq_id y) *' )).| is summable by COMSEQ_1:49;
then A22: (seq_id x) (#) ((seq_id y) *' ) is absolutely_summable by COMSEQ_3:def 13;
A23: (a * x) .|. y = the scalar of Complex_l2_Space . (a * x),y by CSSPACE:def 12
.= Sum ((seq_id (a * x)) (#) ((seq_id y) *' )) by CSSPACE:def 19, CSSPACE:def 20
.= Sum ((seq_id (a (#) (seq_id x))) (#) ((seq_id y) *' )) by Lm14
.= Sum ((a (#) (seq_id x)) (#) ((seq_id y) *' )) by CSSPACE:3
.= Sum (a (#) ((seq_id x) (#) ((seq_id y) *' ))) by COMSEQ_1:15
.= a * (Sum ((seq_id x) (#) ((seq_id y) *' ))) by A22, COMSEQ_3:57
.= a * (the scalar of Complex_l2_Space . x,y) by CSSPACE:def 19, CSSPACE:def 20
.= a * (x .|. y) by CSSPACE:def 12 ;
x .|. y = the scalar of Complex_l2_Space . x,y by CSSPACE:def 12
.= Sum ((seq_id x) (#) ((seq_id y) *' )) by CSSPACE:def 19, CSSPACE:def 20
.= Sum ((((seq_id x) *' ) *' ) (#) ((seq_id y) *' )) by Lm1
.= Sum ((((seq_id x) *' ) (#) (seq_id y)) *' ) by COMSEQ_2:5
.= (Sum (((seq_id x) *' ) (#) (seq_id y))) *' by A17, Lm6
.= (the scalar of Complex_l2_Space . y,x) *' by CSSPACE:def 19, CSSPACE:def 20
.= (y .|. x) *' by CSSPACE:def 12 ;
hence ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) by A4, A12, A2, A3, A15, A18, A21, A23, RSSPACE:20, SERIES_1:21; :: thesis: verum