let p be XFinSequence of ; :: thesis: for Fr being XFinSequence of st p = Fr holds
Sum p = Sum Fr
let Fr be XFinSequence of ; :: 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 & 0 = the_unity_wrt addnat ) by BINOP_2:5, STIRL2_1:def 3;
hence Sum p = Sum Fr by A1, A2, Lm6; :: 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: S₁[ 0 ]

proof

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

end;

A4: 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 A5: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A6: n + 1 in dom p ; :: thesis: Sum (p | ((n + 1) + 1)) = Sum (Fr | ((n + 1) + 1))
then ( n < n + 1 & n + 1 < dom p ) by NAT_1:13, NAT_1:45;
then n < dom p by XXREAL_0:2;
then ( Sum (p | ((n + 1) + 1)) = (p . (n + 1)) + (Sum (p | (n + 1))) & Sum (Fr | ((n + 1) + 1)) = (Fr . (n + 1)) + (Sum (Fr | (n + 1))) & Sum (p | (n + 1)) = Sum (Fr | (n + 1)) ) by A1, A5, A6, Lm8, CARD_FIN:44, NAT_1:45;
hence Sum (p | ((n + 1) + 1)) = Sum (Fr | ((n + 1) + 1)) by A1; :: thesis: verum

end;

A7: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
d1 < d1 + 1 by NAT_1:13;
then ( d1 in dom p & p | (dom p) = p & d1 + 1 = dom p ) by NAT_1:45, RELAT_1:98;
hence Sum p = Sum Fr by A1, A7; :: thesis: verum

end;

end;

end;

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