let p be XFinSequence of NAT ; :: thesis: for Fr being XFinSequence of REAL st p = Fr holds
Sum p = Sum Fr
let Fr be XFinSequence of REAL ; :: thesis: ( p = Fr implies Sum p = Sum Fr )
assume A1: p = Fr ; :: thesis: Sum p = Sum Fr

now

per cases ( dom p = 0 or dom p > 0 ) ;

suppose A2: dom p = 0 ; :: thesis: Sum p = Sum Fr

then len p = 0 ;
then addnat "**" p = the_unity_wrt addnat by STIRL2_1:def 3;
hence Sum p = Sum Fr by A1, A2, Lm6, BINOP_2:5; :: thesis: verum

end;

suppose dom p > 0 ; :: thesis: Sum p = Sum Fr

then reconsider d1 = (dom p) - 1 as Nat by NAT_1:20;
defpred S₁[ Element of NAT ] means ( $1 in dom p implies Sum (p | ($1 + 1)) = Sum (Fr | ($1 + 1)) );
A3: ( p | (dom p) = p & d1 + 1 = dom p ) by RELAT_1:98;
d1 < d1 + 1 by NAT_1:13;
then A4: d1 in dom p by NAT_1:45;
A5: S₁[ 0 ]

proof

assume 0 in dom p ; :: thesis: Sum (p | (0 + 1)) = Sum (Fr | (0 + 1))
then 0 + 1 <= dom p by NAT_1:13;
then A6: 1 c= dom p by NAT_1:40;
then len (p | 1) = 1 by RELAT_1:91;
then A7: p | 1 = <%((p | 1) . 0 )%> by AFINSQ_1:38;
dom (Fr | 1) = 1 by A1, A6, RELAT_1:91;
then Sum (Fr | 1) = (p | 1) . 0 by A1, Lm7;
hence Sum (p | (0 + 1)) = Sum (Fr | (0 + 1)) by A7, STIRL2_1:44; :: thesis: verum

end;

A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A10: n + 1 in dom p ; :: thesis: Sum (p | ((n + 1) + 1)) = Sum (Fr | ((n + 1) + 1))
then n + 1 < dom p by NAT_1:45;
then A11: n < dom p by NAT_1:13;
Sum (p | ((n + 1) + 1)) = (p . (n + 1)) + (Sum (p | (n + 1))) by A10, CARD_FIN:44;
hence Sum (p | ((n + 1) + 1)) = Sum (Fr | ((n + 1) + 1)) by A1, A9, A10, A11, Lm8, NAT_1:45; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A8);
hence Sum p = Sum Fr by A1, A4, A3; :: thesis: verum

end;

end;

end;

hence Sum p = Sum Fr ; :: thesis: verum