let Fr be XFinSequence of REAL ; :: thesis: ex absFr being XFinSequence of REAL st
( dom absFr = dom Fr & |.(Sum Fr).| <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| ) )
defpred S₁[ object , object ] means $2 = |.(Fr . $1).|;
A1: for i being Nat st i in Segm (len Fr) holds
ex x being Element of REAL st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Segm (len Fr) implies ex x being Element of REAL st S₁[i,x] )
assume i in Segm (len Fr) ; :: thesis: ex x being Element of REAL st S₁[i,x]
consider x being Real such that
A2: S₁[i,x] ;
reconsider x = x as Element of REAL by XREAL_0:def 1;
S₁[i,x] by A2;
hence ex x being Element of REAL st S₁[i,x] ; :: thesis: verum

end;

consider absFr being XFinSequence of REAL such that
A3: dom absFr = Segm (len Fr) and
A4: for i being Nat st i in Segm (len Fr) holds
S₁[i,absFr . i] from STIRL2_1:sch 5(A1);
defpred S₂[ Nat] means ( $1 <= len Fr implies |.(Sum (Fr | $1)).| <= Sum (absFr | $1) );
A5: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A6: S₂[i] ; :: thesis: S₂[i + 1]
set i1 = i + 1;
assume A7: i + 1 <= len Fr ; :: thesis: |.(Sum (Fr | (i + 1))).| <= Sum (absFr | (i + 1))
then i < len Fr by NAT_1:13;
then A8: i in dom Fr by AFINSQ_1:86;
then ( Sum (Fr | (i + 1)) = (Fr . i) + (Sum (Fr | i)) & absFr . i = |.(Fr . i).| ) by A4, AFINSQ_2:65;
then A9: |.(Sum (Fr | (i + 1))).| <= (absFr . i) + |.(Sum (Fr | i)).| by COMPLEX1:56;
Sum (absFr | (i + 1)) = (absFr . i) + (Sum (absFr | i)) by A3, A8, AFINSQ_2:65;
then (absFr . i) + |.(Sum (Fr | i)).| <= Sum (absFr | (i + 1)) by A6, A7, NAT_1:13, XREAL_1:7;
hence |.(Sum (Fr | (i + 1))).| <= Sum (absFr | (i + 1)) by A9, XXREAL_0:2; :: thesis: verum

end;

take absFr ; :: thesis: ( dom absFr = dom Fr & |.(Sum Fr).| <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| ) )
A10: S₂[ 0 ] by COMPLEX1:44;
for i being Nat holds S₂[i] from NAT_1:sch 2(A10, A5);
then |.(Sum (Fr | (len Fr))).| <= Sum (absFr | (len Fr)) ;
hence ( dom absFr = dom Fr & |.(Sum Fr).| <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| ) ) by A3, A4; :: thesis: verum