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;
A2: the multF of L is commutative by MONOID_0:def 11;
the multF of L is associative by GROUP_1:31;
hence Product g = Product f by A1, A2, FINSOP_1:8, GROUP_1:34; :: thesis: verum