let L be non empty unital associative commutative multMagma ; :: thesis: for f, g being FinSequence of L
for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
let f, g be FinSequence of L; :: thesis: for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
let p be Permutation of (dom f); :: thesis: ( g = f * p implies Product g = Product f )
assume A1: g = f * p ; :: thesis: Product g = Product f
set mL = the multF of L;
( the multF of L is commutative & the multF of L is associative ) by MONOID_0:def 11;
hence Product g = Product f by A1, FINSOP_1:7; :: thesis: verum