let L be non empty unital associative commutative multMagma ; :: thesis: for f, g being FinSequence of
for p being Permutation of dom f st g = f * p holds
Product g = Product f
let f, g be FinSequence of ; :: 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 GROUP_1:31, MONOID_0:def 11;
hence Product g = Product f by A1, FINSOP_1:8, GROUP_1:34; :: thesis: verum