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:8
.= ((Product f2) " ) * ((Product f1) " ) by GROUP_1:25 ; :: thesis: verum