reconsider a = (1 / 2) + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
reconsider x = a GeoSeq as Complex_Sequence ;
A1: for m being Nat holds |.x.| . (m + 1) = (|.x.| . m) * |.a.|
proof
let m be Nat; :: thesis: |.x.| . (m + 1) = (|.x.| . m) * |.a.|
|.x.| . (m + 1) = |.(x . (m + 1)).| by VALUED_1:18
.= |.((x . m) * a).| by COMSEQ_3:def 1
.= |.(x . m).| * |.a.| by COMPLEX1:65 ;
hence |.x.| . (m + 1) = (|.x.| . m) * |.a.| by VALUED_1:18; :: thesis: verum
end;
|.x.| . 0 = |.(x . 0).| by VALUED_1:18
.= 1 by COMPLEX1:48, COMSEQ_3:def 1 ;
then ( |.a.| = 1 / 2 & |.x.| = |.a.| GeoSeq ) by A1, ABSVALUE:def 1, PREPOWER:3;
then |.x.| is summable by SERIES_1:24;
then x is absolutely_summable by COMSEQ_3:def 9;
then seq_id x is absolutely_summable by CSSPACE:1;
then reconsider v = x as VECTOR of Complex_l1_Space by CSSPACE3:6;
(seq_id v) . 0 = x . 0 by CSSPACE:1
.= 1 by COMPLEX1:def 4, COMSEQ_3:def 1 ;
then v <> CZeroseq by CSSPACE:4;
hence not Complex_l1_Space is trivial by CSSPACE3:6; :: thesis: verum