let R be Ring; :: thesis: for S being Subring of R
for a being FinSequence of S
for A being FinSequence of R st a = A holds
Sum a = Sum A
let S be Subring of R; :: thesis: for a being FinSequence of S
for A being FinSequence of R st a = A holds
Sum a = Sum A
defpred S₁[ Nat] means for a being FinSequence of S
for A being FinSequence of R st a = A & len a = $1 holds
Sum a = Sum A;
A1: S₁[ 0 ]

proof

let a be FinSequence of S; :: thesis: for A being FinSequence of R st a = A & len a = 0 holds
Sum a = Sum A
let A be FinSequence of R; :: thesis: ( a = A & len a = 0 implies Sum a = Sum A )
assume A2: ( a = A & len a = 0 ) ; :: thesis: Sum a = Sum A
hence Sum a = 0. S by RLVECT_1:75
.= 0. R by C0SP1:def 3
.= Sum A by A2, RLVECT_1:75 ;
:: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let a be FinSequence of S; :: thesis: for A being FinSequence of R st a = A & len a = k + 1 holds
Sum a = Sum A
let A be FinSequence of R; :: thesis: ( a = A & len a = k + 1 implies Sum a = Sum A )
assume A5: ( a = A & len a = k + 1 ) ; :: thesis: Sum a = Sum A
then consider a0 being FinSequence of S, aN being Element of S such that
A6: a = a0 ^ <*aN*> by FINSEQ_2:19;
consider A0 being FinSequence of R, AN being Element of R such that
A7: A = A0 ^ <*AN*> by A5, FINSEQ_2:19;
A8: ( a0 = A0 & aN = AN ) by A5, A7, A6, FINSEQ_2:17;
k + 1 = (len a0) + 1 by A5, A6, FINSEQ_2:16;
then A9: Sum a0 = Sum A0 by A4, A8;
A10: Sum <*aN*> = aN by RLVECT_1:44
.= Sum <*AN*> by A8, RLVECT_1:44 ;
thus Sum a = (Sum a0) + (Sum <*aN*>) by A6, RLVECT_1:41
.= (Sum A0) + (Sum <*AN*>) by A9, A10, FIELD_6:15
.= Sum A by A7, RLVECT_1:41 ; :: thesis: verum

end;

A11: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
let a be FinSequence of S; :: thesis: for A being FinSequence of R st a = A holds
Sum a = Sum A
let A be FinSequence of R; :: thesis: ( a = A implies Sum a = Sum A )
assume A12: a = A ; :: thesis: Sum a = Sum A
S₁[ len a] by A11;
hence Sum a = Sum A by A12; :: thesis: verum