let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: Sum (^ F) = ^ (Sum F)
set L = INT.Ring ;
set PRI = Polynom-Ring INT.Ring;
A1: Seg (len (^ F)) = dom (^ F) by FINSEQ_1:def 3
.= dom F by Def7
.= Seg (len F) by FINSEQ_1:def 3 ;

per cases ( len F = 0 or len F <> 0 ) ;

suppose A2: len F = 0 ; :: thesis: Sum (^ F) = ^ (Sum F)

then F = <*> the carrier of (Polynom-Ring INT.Ring) ;
then A4: Sum F = 0. (Polynom-Ring INT.Ring) by RLVECT_1:43;
^ F = <*> the carrier of (Polynom-Ring F_Real) by A2, A1;
then Sum (^ F) = 0. (Polynom-Ring F_Real) by RLVECT_1:43;
hence Sum (^ F) = ^ (Sum F) by A4, FIELD_4:11; :: thesis: verum

end;

suppose A6: len F <> 0 ; :: thesis: Sum (^ F) = ^ (Sum F)

for k being non zero Nat st len F = k holds
Sum (^ F) = ^ (Sum F)

proof

let k be non zero Nat; :: thesis: ( len F = k implies Sum (^ F) = ^ (Sum F) )
defpred S₁[ Nat] means for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len F = $1 holds
Sum (^ F) = ^ (Sum F);
A7: S₁[1]

proof

for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len F = 1 holds
Sum (^ F) = ^ (Sum F)

proof

let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len F = 1 implies Sum (^ F) = ^ (Sum F) )
assume A8: len F = 1 ; :: thesis: Sum (^ F) = ^ (Sum F)
then dom F = Seg 1 by FINSEQ_1:def 3;
then A9: 1 in dom F ;
then F . 1 in rng F by FUNCT_1:3;
then reconsider F1 = F . 1 as Element of (Polynom-Ring INT.Ring) ;
A10: Seg (len (^ F)) = dom (^ F) by FINSEQ_1:def 3
.= dom F by Def7
.= Seg (len F) by FINSEQ_1:def 3 ;
A11: F = <*F1*> by A8, FINSEQ_1:40;
F /. 1 = F1 by A9, PARTFUN1:def 6;
then A13: (^ F) . 1 = ^ F1 by A9, Def7;
reconsider RF1 = ^ F1 as Element of (Polynom-Ring F_Real) ;
reconsider RF = ^ F as FinSequence of the carrier of (Polynom-Ring F_Real) ;
A14: RF = <*(^ F1)*> by A13, A8, A10, FINSEQ_1:6, FINSEQ_1:40;
Sum RF = ^ F1 by BINOM:3, A14;
hence Sum (^ F) = ^ (Sum F) by BINOM:3, A11; :: thesis: verum

end;

hence S₁[1] ; :: thesis: verum

end;

A15: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A16: S₁[k] ; :: thesis: S₁[k + 1]
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len F = k + 1 holds
Sum (^ F) = ^ (Sum F)

proof

let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len F = k + 1 implies Sum (^ F) = ^ (Sum F) )
assume A17: len F = k + 1 ; :: thesis: Sum (^ F) = ^ (Sum F)
then consider G being FinSequence of (Polynom-Ring INT.Ring), d being Element of (Polynom-Ring INT.Ring) such that
A18: F = G ^ <*d*> by FINSEQ_2:19;
A19: Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (^ F) by Def7
.= Seg (len (^ F)) by FINSEQ_1:def 3 ;
dom F = Seg (k + 1) by A17, FINSEQ_1:def 3;
then A20: dom (^ F) = Seg (k + 1) by Def7;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*> by A18, A17, FINSEQ_5:21;
then A21: ( G = F | k & d = F /. (len F) ) by FINSEQ_2:17;
A22: k + 1 = (len G) + 1 by FINSEQ_2:16, A18, A17;
reconsider RF = ^ F as FinSequence of the carrier of (Polynom-Ring F_Real) ;
len F in Seg (len F) by A17, FINSEQ_1:3;
then A23: len F in dom F by FINSEQ_1:def 3;
reconsider Fl = F /. (len F) as Element of the carrier of (Polynom-Ring INT.Ring) ;
A24: len RF = len F by A19, FINSEQ_1:6;
len RF in dom F by A19, FINSEQ_1:6, A23;
then len RF in dom RF by Def7;
then A25: RF /. (len RF) = RF . (len RF) by PARTFUN1:def 6
.= (^ F) . (len F) by A19, FINSEQ_1:6
.= ^ Fl by A23, Def7 ;
Sum F = (Sum G) + d by A18, FVSUM_1:71;
then ^ (Sum F) = (^ (Sum G)) + (^ d) by Th27
.= (Sum (^ (F | k))) + (^ (F /. (len F))) by A22, A16, A21
.= (Sum ((^ F) | k)) + (^ Fl) by A17, Lm16
.= Sum (((^ F) | k) ^ <*(^ Fl)*>) by FVSUM_1:71
.= Sum (RF | (k + 1)) by A24, A17, FINSEQ_5:82, A25
.= Sum (^ F) by A20 ;
hence Sum (^ F) = ^ (Sum F) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A7, A15);
hence ( len F = k implies Sum (^ F) = ^ (Sum F) ) ; :: thesis: verum

end;

hence Sum (^ F) = ^ (Sum F) by A6; :: thesis: verum

end;

end;