let G be Group; :: thesis: for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
let f1, f2 be FinSequence of G; :: thesis: (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
thus (Product (f1 ^ f2)) " = ((Product f1) * (Product f2)) " by GROUP_4:5
.= ((Product f2) ") * ((Product f1) ") by GROUP_1:17 ; :: thesis: verum