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
Product F = Product G
let S be Subring of R; :: thesis: for F being FinSequence of R
for G being FinSequence of S st F = G holds
Product F = Product G
let F be FinSequence of R; :: thesis: for G being FinSequence of S st F = G holds
Product F = Product G
let G be FinSequence of S; :: thesis: ( F = G implies Product F = Product G )
assume AS: F = G ; :: thesis: Product F = Product G
the carrier of S c= the carrier of R by C0SP1:def 3;
then In ((Product G),R) = Product G by SUBSET_1:def 8;
hence Product F = Product G by AS, Th14; :: thesis: verum