let Fr be XFinSequence of ; :: thesis: ex absFr being XFinSequence of st
( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = abs (Fr . i) ) )
defpred S₁[ set , set ] means $2 = abs (Fr . $1);
A1: Fr | (dom Fr) = Fr by RELAT_1:98;
A2: for i being Nat st i in len Fr holds
ex x being Element of REAL st S₁[i,x] ;
consider absFr being XFinSequence of such that
A3: dom absFr = len Fr and
A4: for i being Nat st i in len Fr holds
S₁[i,absFr . i] from STIRL2_1:sch 5(A2);
defpred S₂[ Nat] means ( $1 <= len Fr implies abs (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: abs (Sum (Fr | (i + 1))) <= Sum (absFr | (i + 1))
then i < len Fr by NAT_1:13;
then A8: i in dom Fr by NAT_1:45;
then ( Sum (Fr | (i + 1)) = (Fr . i) + (Sum (Fr | i)) & absFr . i = abs (Fr . i) ) by A4, AFINSQ_2:77;
then A9: abs (Sum (Fr | (i + 1))) <= (absFr . i) + (abs (Sum (Fr | i))) by COMPLEX1:142;
Sum (absFr | (i + 1)) = (absFr . i) + (Sum (absFr | i)) by A3, A8, AFINSQ_2:77;
then (absFr . i) + (abs (Sum (Fr | i))) <= Sum (absFr | (i + 1)) by A6, A7, NAT_1:13, XREAL_1:9;
hence abs (Sum (Fr | (i + 1))) <= Sum (absFr | (i + 1)) by A9, XXREAL_0:2; :: thesis: verum

end;

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