let G be Group; :: thesis: for f being FinSequence of G holds (Product f) " = Product ((Rev f) " )
let f be FinSequence of G; :: thesis: (Product f) " = Product ((Rev f) " )
A1: Product (((Rev f) " ) ^ f) = 1_ G by Th25;
Product (f ^ ((Rev f) " )) = 1_ G by Th24;
then ( (Product f) * (Product ((Rev f) " )) = 1_ G & (Product ((Rev f) " )) * (Product f) = 1_ G ) by A1, GROUP_4:8;
hence (Product f) " = Product ((Rev f) " ) by GROUP_1:12; :: thesis: verum