let G be non empty unital associative multMagma ; :: thesis: for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2)
let F1, F2 be FinSequence of the carrier of G; :: thesis: Product (F1 ^ F2) = (Product F1) * (Product F2)
set g = the multF of G;
the multF of G is associative by GROUP_1:31;
hence Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:6, GROUP_1:34; :: thesis: verum