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 17, CSSPACE:def 18 ;
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:53;
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:12;

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 17, CSSPACE:def 18 ;
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:7
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) + (- (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n)) by SEQ_1:10
.= (((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:8
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by SEQ_1:8
.= ((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:27
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (- (Im ((seq_id x) . n)))) by COMPLEX1:27
.= ((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:63;
( (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:63;
then (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A8, XREAL_1:7;
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:53;
then A10: Sum (Re ((seq_id x) (#) ((seq_id x) *'))) = 0 by COMPLEX1:4, COMPLEX1:12;
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:17;
hence (seq_id x) . n = 0 by COMPLEX1:5; :: thesis: verum

end;

x is Element of the_set_of_ComplexSequences by CSSPACE:def 11, CSSPACE:def 18;
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 17, CSSPACE:def 18
.= 0 by A14, CSSPACE:80 ; :: 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:63;
(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:40 ;
then (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A16, XREAL_1:7;
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:46;
then A17: ((seq_id x) *') (#) (seq_id y) is absolutely_summable by COMSEQ_3:def 9;
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:40; :: 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:46;
then A19: (seq_id x) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def 9;
|.(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:46;
then A20: (seq_id y) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def 9;
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 17, CSSPACE:def 18
.= 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:1
.= Sum (((seq_id x) (#) ((seq_id z) *')) + ((seq_id y) (#) ((seq_id z) *'))) by COMSEQ_1:10
.= (Sum ((seq_id x) (#) ((seq_id z) *'))) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by A19, A20, COMSEQ_3:54
.= ( the scalar of Complex_l2_Space . (x,z)) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by CSSPACE:def 17, CSSPACE:def 18
.= ( the scalar of Complex_l2_Space . (x,z)) + ( the scalar of Complex_l2_Space . (y,z)) by CSSPACE:def 17, CSSPACE:def 18
.= (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:46;
then A22: (seq_id x) (#) ((seq_id y) *') is absolutely_summable by COMSEQ_3:def 9;
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 17, CSSPACE:def 18
.= Sum ((seq_id (a (#) (seq_id x))) (#) ((seq_id y) *')) by Lm14
.= Sum ((a (#) (seq_id x)) (#) ((seq_id y) *')) by CSSPACE:1
.= Sum (a (#) ((seq_id x) (#) ((seq_id y) *'))) by COMSEQ_1:12
.= a * (Sum ((seq_id x) (#) ((seq_id y) *'))) by A22, COMSEQ_3:56
.= a * ( the scalar of Complex_l2_Space . (x,y)) by CSSPACE:def 17, CSSPACE:def 18
.= 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 17, CSSPACE:def 18
.= 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 17, CSSPACE:def 18
.= (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:16, SERIES_1:18; :: thesis: verum