set a = 1 / 2;

reconsider x = (1 / 2) GeoSeq as Real_Sequence ;

A1: |.(1 / 2).| = 1 / 2 by ABSVALUE:def 1;

defpred S_{1}[ Nat] means 0 <= x . c_{1};

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by PREPOWER:3;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2);

then x is absolutely_summable by A1, SERIES_1:24, SERIES_1:36;

then seq_id x is absolutely_summable ;

then reconsider v = x as VECTOR of l1_Space by RSSPACE3:6;

(seq_id v) . 0 = 1 by PREPOWER:3;

then v <> seq_id Zeroseq by RSSPACE:4;

hence not l1_Space is trivial by RSSPACE3:6; :: thesis: verum

reconsider x = (1 / 2) GeoSeq as Real_Sequence ;

A1: |.(1 / 2).| = 1 / 2 by ABSVALUE:def 1;

defpred S

A2: for n being Nat st S

S

proof

A4:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3;

hence ( S_{1}[n] implies S_{1}[n + 1] )
; :: thesis: verum

end;x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3;

hence ( S

for n being Nat holds S

then x is absolutely_summable by A1, SERIES_1:24, SERIES_1:36;

then seq_id x is absolutely_summable ;

then reconsider v = x as VECTOR of l1_Space by RSSPACE3:6;

(seq_id v) . 0 = 1 by PREPOWER:3;

then v <> seq_id Zeroseq by RSSPACE:4;

hence not l1_Space is trivial by RSSPACE3:6; :: thesis: verum