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

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