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