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

A1: now :: thesis: for p being FinSequence of the carrier of F_Complex
for x being Element of the carrier of F_Complex st S₁[p] holds
S₁[p ^ <*x*>]

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:6;
Sum (p ^ <*x*>) = (Sum p) + x by FVSUM_1:71;
then A3: |.(Sum (p ^ <*x*>)).| <= |.(Sum p).| + |.x.| by COMPLFLD:62;
reconsider xx = |.x.| as Element of REAL by XREAL_0:def 1;
(Sum |.p.|) + |.x.| = (Sum |.p.|) + (Sum <*xx*>) by FINSOP_1:11
.= (Sum |.p.|) + (Sum |.<*x*>.|) by Th9
.= Sum (|.p.| ^ |.<*x*>.|) by RVSUM_1:75
.= Sum |.(p ^ <*x*>).| by Th12 ;
hence S₁[p ^ <*x*>] by A2, A3, XXREAL_0:2; :: thesis: verum

end;

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