set D = the carrier of F_Complex;
defpred S1[ 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 S1[p] holds
S1[p ^ <*x*>]
let p be FinSequence of the carrier of F_Complex; :: thesis: for x being Element of the carrier of F_Complex st S1[p] holds
S1[p ^ <*x*>]
let x be Element of the carrier of F_Complex; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume S1[p] ; :: thesis: S1[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 S1[p ^ <*x*>] by A2, A3, XXREAL_0:2; :: thesis: verum
end;
A4: S1[ <*> 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 S1[p] from FINSEQ_2:sch 2(A4, A1); :: thesis: verum