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

A1: now

assume A2: x .|. x = 0 ; :: thesis: x = 0. Complex_l2_Space
A3: 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 ;
(seq_id x) (#) ((seq_id x) *' ) is absolutely_summable by Lm20;
then A4: (seq_id x) (#) ((seq_id x) *' ) is summable ;
then (Sum (Re ((seq_id x) (#) ((seq_id x) *' )))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *' )))) * <i> ) = 0 by A2, A3, COMSEQ_3:54;
then A5: ( Sum (Re ((seq_id x) (#) ((seq_id x) *' ))) = 0 & Sum (Im ((seq_id x) (#) ((seq_id x) *' ))) = 0 ) by COMPLEX1:12, COMPLEX1:28;
set seq = seq_id x;
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 3
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *' )) . n)) by COMSEQ_3:def 3
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - ((Im ((seq_id x) . n)) * ((Im ((seq_id x) *' )) . n)) by COMSEQ_3:def 4
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *' ) . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *' ) . n))) by COMSEQ_3:def 4
.= ((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 ) & Re ((seq_id x) (#) ((seq_id x) *' )) is summable )

proof

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: (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = ((Re ((seq_id x) . n)) ^2 ) + ((Im ((seq_id x) . n)) ^2 ) by A6;
( (Re ((seq_id x) . n)) ^2 >= 0 & (Im ((seq_id x) . n)) ^2 >= 0 ) by 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;

hence ( ( for n being Element of NAT holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n ) & Re ((seq_id x) (#) ((seq_id x) *' )) is summable ) by A4; :: thesis: verum

end;

A9: 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 A5, 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 A9, Lm11, CSSPACE:def 6; :: thesis: verum

end;

A10: now

assume A11: x = 0. Complex_l2_Space ; :: thesis: x .|. x = 0
A12: 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 A11, 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 A12, CSSPACE:88 ; :: thesis: verum

end;

set seqx = seq_id x;
(seq_id x) (#) ((seq_id x) *' ) is absolutely_summable by Lm20;
then A13: (seq_id x) (#) ((seq_id x) *' ) is summable ;
A14: ( Re (x .|. x) >= 0 & Im (x .|. x) = 0 )

proof

A15: 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 ;
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 A13, COMSEQ_3:54;
then A16: ( Re (x .|. x) = Sum (Re ((seq_id x) (#) ((seq_id x) *' ))) & Im (x .|. x) = Sum (Im ((seq_id x) (#) ((seq_id x) *' ))) ) by A15, COMPLEX1:28;
A17: ( Re ((seq_id x) (#) ((seq_id x) *' )) is summable & Im ((seq_id x) (#) ((seq_id x) *' )) is summable ) by A13;
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
A18: (Re ((seq_id x) (#) ((seq_id x) *' ))) . n = Re (((seq_id x) (#) ((seq_id x) *' )) . n) by COMSEQ_3:def 3
.= 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 ;
( (Re ((seq_id x) . n)) ^2 >= 0 & (Im ((seq_id x) . n)) ^2 >= 0 ) by XREAL_1:65;
then (Re ((seq_id x) (#) ((seq_id x) *' ))) . n >= 0 + 0 by A18, XREAL_1:9;
hence 0 <= (Re ((seq_id x) (#) ((seq_id x) *' ))) . n ; :: thesis: verum

end;

hence Re (x .|. x) >= 0 by A16, A17, SERIES_1:21; :: thesis: Im (x .|. x) = 0
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 4
.= 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;

hence Im (x .|. x) = 0 by A16, RSSPACE:20; :: thesis: verum

end;

set seqy = seq_id y;
set seqz = seq_id z;
|.(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 A19: ((seq_id x) *' ) (#) (seq_id y) is absolutely_summable by COMSEQ_3:def 11;
A20: 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 A19, Lm6
.= (the scalar of Complex_l2_Space . y,x) *' by CSSPACE:def 19, CSSPACE:def 20
.= (y .|. x) *' by CSSPACE:def 12 ;
|.(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 (seq_id x) (#) ((seq_id z) *' ) is absolutely_summable by COMSEQ_3:def 11;
then A21: (seq_id x) (#) ((seq_id z) *' ) is summable ;
|.(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 (seq_id y) (#) ((seq_id z) *' ) is absolutely_summable by COMSEQ_3:def 11;
then A22: (seq_id y) (#) ((seq_id z) *' ) is summable ;
A23: (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 A21, A22, 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 (seq_id x) (#) ((seq_id y) *' ) is absolutely_summable by COMSEQ_3:def 11;
then A24: (seq_id x) (#) ((seq_id y) *' ) is summable ;
(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 A24, 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 ;
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 A1, A10, A14, A20, A23; :: thesis: verum