let R be Ring; :: thesis: for S being Subring of R
for f being FinSequence of R
for g being FinSequence of S st f = g holds
Sum f = Sum g
let S be Subring of R; :: thesis: for f being FinSequence of R
for g being FinSequence of S st f = g holds
Sum f = Sum g
let f be FinSequence of R; :: thesis: for g being FinSequence of S st f = g holds
Sum f = Sum g
let g be FinSequence of S; :: thesis: ( f = g implies Sum f = Sum g )
assume AS: f = g ; :: thesis: Sum f = Sum g
defpred S₁[ Nat] means for f being FinSequence of R
for g being FinSequence of S st f = g & len f = $1 holds
Sum f = Sum g;

now :: thesis: for f being FinSequence of R
for g being FinSequence of S st f = g & len f = 0 holds
Sum f = Sum g

let f be FinSequence of R; :: thesis: for g being FinSequence of S st f = g & len f = 0 holds
Sum f = Sum g
let g be FinSequence of S; :: thesis: ( f = g & len f = 0 implies Sum f = Sum g )
assume ( f = g & len f = 0 ) ; :: thesis: Sum f = Sum g
then A: ( f = <*> the carrier of R & g = <*> the carrier of S ) ;
hence Sum f = 0. R by RLVECT_1:43
.= 0. S by C0SP1:def 3
.= Sum g by A, RLVECT_1:43 ;
:: thesis: verum

end;

then A: S₁[ 0 ] ;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IA: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being FinSequence of R
for g being FinSequence of S st f = g & len f = k + 1 holds
Sum f = Sum g

let f be FinSequence of R; :: thesis: for g being FinSequence of S st f = g & len f = k + 1 holds
Sum f = Sum g
let g be FinSequence of S; :: thesis: ( f = g & len f = k + 1 implies Sum f = Sum g )
assume B0: ( f = g & len f = k + 1 ) ; :: thesis: Sum f = Sum g
then g <> {} ;
then consider h being FinSequence, x being object such that
B1: g = h ^ <*x*> by FINSEQ_1:46;
reconsider h = h, o = <*x*> as FinSequence of S by B1, FINSEQ_1:36;
len o = 1 by FINSEQ_1:39;
then B2: len g = (len h) + 1 by B1, FINSEQ_1:22;
C2: dom g = Seg (k + 1) by B0, FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
x = g . (k + 1) by B0, B2, B1, FINSEQ_1:42;
then reconsider x = x as Element of S by B4, C2, FINSEQ_1:1, FINSEQ_2:11;
reconsider y = x as Element of R by AS4;
rng h c= the carrier of R by AS4;
then reconsider hh = h as FinSequence of R by FINSEQ_1:def 4;
rng o c= the carrier of R by AS4;
then reconsider oo = o as FinSequence of R by FINSEQ_1:def 4;
dom the addF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then B7: [(Sum h),(Sum o)] in dom the addF of S ;
B8: Sum o = y by RLVECT_1:44
.= Sum oo by RLVECT_1:44 ;
thus Sum f = (Sum hh) + (Sum oo) by B0, B1, RLVECT_1:41
.= the addF of R . ((Sum h),(Sum o)) by B8, B0, B2, IA
.= ( the addF of R || the carrier of S) . ((Sum h),(Sum o)) by B7, FUNCT_1:49
.= (Sum h) + (Sum o) by C0SP1:def 3
.= Sum g by B1, RLVECT_1:41 ; :: thesis: verum

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider n being Nat such that
H: len f = n ;
thus Sum f = Sum g by AS, I, H; :: thesis: verum