set a = 1 / 2;
reconsider x = (1 / 2) GeoSeq as Real_Sequence ;
A1: abs (1 / 2) = 1 / 2 by ABSVALUE:def 1;
defpred S₁[ Element of NAT ] means 0 <= x . c₁;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A3: x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3;
assume S₁[n] ; :: thesis: S₁[n + 1]
hence S₁[n + 1] by A3; :: thesis: verum

end;

A4: S₁[ 0 ] by PREPOWER:3;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2);
then x is absolutely_summable by A1, SERIES_1:24, SERIES_1:36;
then seq_id x is absolutely_summable by RSSPACE:1;
then reconsider v = x as VECTOR of l1_Space by RSSPACE3:6;
(seq_id v) . 0 = x . 0 by RSSPACE:1
.= 1 by PREPOWER:3 ;
then v <> Zeroseq by RSSPACE:def 6;
hence not l1_Space is trivial by RSSPACE3:6, STRUCT_0:def 18; :: thesis: verum