let Fr be XFinSequence of REAL ; :: thesis: ex absFr being XFinSequence of REAL st
( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Element of NAT st i in dom absFr holds
absFr . i = abs (Fr . i) ) )
defpred S1[ set , set ] means $2 = abs (Fr . $1);
A1: for i being Element of NAT st i in len Fr holds
ex x being Element of REAL st S1[i,x] ;
consider absFr being XFinSequence of REAL such that
A2: dom absFr = len Fr and
A3: for i being Element of NAT st i in len Fr holds
S1[i,absFr . i] from STIRL2_1:sch 6(A1);
 take absFr ; :: thesis: ( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Element of NAT st i in dom absFr holds
absFr . i = abs (Fr . i) ) )
defpred S2[ Element of NAT ] means ( $1 <= len Fr implies abs (Sum (Fr | $1)) <= Sum (absFr | $1) );
A4: S2[ 0 ]
proof
( Sum (Fr | 0 ) = 0 & Sum (absFr | 0 ) = 0 ) by Lm6, RELAT_1:60;
hence S2[ 0 ] by COMPLEX1:130; :: thesis: verum
end;
A5: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
assume A6: S2[i] ; :: thesis: S2[i + 1]
set i1 = i + 1;
assume i + 1 <= len Fr ; :: thesis: abs (Sum (Fr | (i + 1))) <= Sum (absFr | (i + 1))
then ( i < len Fr & len Fr = dom Fr ) by NAT_1:13;
then ( i in dom Fr & i in len Fr & i <= len Fr ) by NAT_1:45;
then ( Sum (Fr | (i + 1)) = (Fr . i) + (Sum (Fr | i)) & Sum (absFr | (i + 1)) = (absFr . i) + (Sum (absFr | i)) & abs (Sum (Fr | i)) <= Sum (absFr | i) & absFr . i = abs (Fr . i) ) by A2, A3, A6, Lm8;
then ( abs (Sum (Fr | (i + 1))) <= (absFr . i) + (abs (Sum (Fr | i))) & (absFr . i) + (abs (Sum (Fr | i))) <= Sum (absFr | (i + 1)) ) by COMPLEX1:142, XREAL_1:9;
hence abs (Sum (Fr | (i + 1))) <= Sum (absFr | (i + 1)) by XXREAL_0:2; :: thesis: verum
end;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A4, A5);
 then ( abs (Sum (Fr | (len Fr))) <= Sum (absFr | (len Fr)) & len Fr = dom Fr & Fr | (dom Fr) = Fr & absFr | (dom absFr) = absFr ) by RELAT_1:98;
hence ( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Element of NAT st i in dom absFr holds
absFr . i = abs (Fr . i) ) ) by A2, A3; :: thesis: verum