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 A1: F = G ; :: thesis: Sum F = Sum G

the carrier of S c= the carrier of R by C0SP1:def 3;

then In ((Sum G),R) = Sum G by SUBSET_1:def 8;

hence Sum F = Sum G by A1, ALGNUM_1:10; :: thesis: verum

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 A1: F = G ; :: thesis: Sum F = Sum G

the carrier of S c= the carrier of R by C0SP1:def 3;

then In ((Sum G),R) = Sum G by SUBSET_1:def 8;

hence Sum F = Sum G by A1, ALGNUM_1:10; :: thesis: verum