let G be non empty unital associative multMagma ; :: thesis: for F being FinSequence of the carrier of G
for a being Element of G holds Product (<*a*> ^ F) = a * (Product F)
let F be FinSequence of the carrier of G; :: thesis: for a being Element of G holds Product (<*a*> ^ F) = a * (Product F)
let a be Element of G; :: thesis: Product (<*a*> ^ F) = a * (Product F)
set g = the multF of G;
( the multF of G is associative & the multF of G is having_a_unity ) by GROUP_1:31, GROUP_1:34;
hence Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:7; :: thesis: verum