set D = the carrier of F_Complex ;
defpred S₁[ FinSequence of the carrier of F_Complex ] means |.(Sum $1).| <= Sum |.$1.|;

A1: now

let p be FinSequence of the carrier of F_Complex ; :: thesis: for x being Element of the carrier of F_Complex st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of the carrier of F_Complex ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume S₁[p] ; :: thesis: S₁[p ^ <*x*>]
then A2: |.(Sum p).| + |.x.| <= (Sum |.p.|) + |.x.| by XREAL_1:8;
Sum (p ^ <*x*>) = (Sum p) + x by FVSUM_1:87;
then A3: |.(Sum (p ^ <*x*>)).| <= |.(Sum p).| + |.x.| by COMPLFLD:100;
(Sum |.p.|) + |.x.| = (Sum |.p.|) + (Sum <*|.x.|*>) by FINSOP_1:12
.= (Sum |.p.|) + (Sum |.<*x*>.|) by Th10
.= Sum (|.p.| ^ |.<*x*>.|) by RVSUM_1:105
.= Sum |.(p ^ <*x*>).| by Th13 ;
hence S₁[p ^ <*x*>] by A2, A3, XXREAL_0:2; :: thesis: verum

end;

A4: S₁[ <*> the carrier of F_Complex ] by Th9, COMPLFLD:93, RLVECT_1:60, RVSUM_1:102;
thus for p being FinSequence of the carrier of F_Complex holds S₁[p] from FINSEQ_2:sch 2(A4, A1); :: thesis: verum