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 by GROUP_1:31;
hence Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:7, GROUP_1:34; :: thesis: verum