let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for a being Element of K
for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)
let a be Element of K; :: thesis: for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)
let p1 be FinSequence of the carrier of K; :: thesis: Product (<*a*> ^ p1) = a * (Product p1)
thus Product (<*a*> ^ p1) = (Product <*a*>) * (Product p1) by GROUP_4:5
.= a * (Product p1) by FINSOP_1:11 ; :: thesis: verum