set a = 1 / 2;
reconsider x = (1 / 2) GeoSeq as Real_Sequence ;
A1: |.(1 / 2).| = 1 / 2 by ABSVALUE:def 1;
defpred S1[ Nat] means 0 <= x . c1;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3;
hence ( S1[n] implies S1[n + 1] ) ; :: thesis: verum
end;
A4: S1[ 0 ] by PREPOWER:3;
for n being Nat holds S1[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