theorem Th90: :: MATGRP_0:77

for R being Ring
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