let x, y, z be Point of l2_Space; :: thesis: for a being Real holds
( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Real; :: thesis: ( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A1: for n being Nat holds 0 <= ((seq_id x) (#) (seq_id x)) . n

proof

let n be Nat; :: thesis: 0 <= ((seq_id x) (#) (seq_id x)) . n
((seq_id x) (#) (seq_id x)) . n = ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8;
hence 0 <= ((seq_id x) (#) (seq_id x)) . n by XREAL_1:63; :: thesis: verum

end;

A2: ( (seq_id x) (#) (seq_id x) is summable & x .|. x = Sum ((seq_id x) (#) (seq_id x)) ) by Th1;

A3: now :: thesis: ( x .|. x = 0 implies x = 0. l2_Space )

A4: for n being Nat holds 0 <= ((seq_id x) (#) (seq_id x)) . n

proof

let n be Nat; :: thesis: 0 <= ((seq_id x) (#) (seq_id x)) . n
((seq_id x) (#) (seq_id x)) . n = ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8;
hence 0 <= ((seq_id x) (#) (seq_id x)) . n by XREAL_1:63; :: thesis: verum

end;

assume A5: x .|. x = 0 ; :: thesis: x = 0. l2_Space
A6: ( x .|. x = Sum ((seq_id x) (#) (seq_id x)) & (seq_id x) (#) (seq_id x) is summable ) by Th1;
A7: for n being Nat holds 0 = (seq_id x) . n

proof

let n be Nat; :: thesis: 0 = (seq_id x) . n
0 = ((seq_id x) (#) (seq_id x)) . n by A5, A4, A6, RSSPACE:17
.= ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8 ;
hence 0 = (seq_id x) . n by XCMPLX_1:6; :: thesis: verum

end;

x is Element of the_set_of_RealSequences by RSSPACE:def 11;
hence x = 0. l2_Space by A7, Th1, RSSPACE:5; :: thesis: verum

end;

A8: x .|. y = Sum ((seq_id x) (#) (seq_id y)) by Th1
.= y .|. x by Th1 ;

A9: now :: thesis: ( x = 0. l2_Space implies x .|. x = 0 )

assume A10: x = 0. l2_Space ; :: thesis: x .|. x = 0
A11: for n being Nat holds ((seq_id x) (#) (seq_id x)) . n = 0

proof

let n be 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 SEQ_1:8
.= ((seq_id x) . n) * 0 by A10, Th1
.= 0 ; :: thesis: verum

end;

thus x .|. x = Sum ((seq_id x) (#) (seq_id x)) by Th1
.= 0 by A11, RSSPACE:16 ; :: thesis: verum

end;

A12: (seq_id x) (#) (seq_id y) is summable by Th1;
A13: (a * x) .|. y = Sum ((seq_id (a * x)) (#) (seq_id y)) by Th1
.= Sum ((a (#) (seq_id x)) (#) (seq_id y)) by Th1
.= Sum (a (#) ((seq_id x) (#) (seq_id y))) by SEQ_1:18
.= a * (Sum ((seq_id x) (#) (seq_id y))) by A12, SERIES_1:10
.= a * (x .|. y) by Th1 ;
A14: ( (seq_id x) (#) (seq_id z) is summable & (seq_id y) (#) (seq_id z) is summable ) by Th1;
(x + y) .|. z = Sum ((seq_id (x + y)) (#) (seq_id z)) by Th1
.= Sum (((seq_id x) + (seq_id y)) (#) (seq_id z)) by Th1
.= Sum (((seq_id x) (#) (seq_id z)) + ((seq_id y) (#) (seq_id z))) by SEQ_1:16
.= (Sum ((seq_id x) (#) (seq_id z))) + (Sum ((seq_id y) (#) (seq_id z))) by A14, SERIES_1:7
.= (x .|. z) + (Sum ((seq_id y) (#) (seq_id z))) by Th1
.= (x .|. z) + (y .|. z) by Th1 ;
hence ( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) by A3, A9, A1, A2, A8, A13, SERIES_1:18; :: thesis: verum