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) " )
Product (f ^ ((Rev f) " )) = 1_ G by Th24;
then A1: (Product f) * (Product ((Rev f) " )) = 1_ G by GROUP_4:8;
Product (((Rev f) " ) ^ f) = 1_ G by Th25;
then (Product ((Rev f) " )) * (Product f) = 1_ G by GROUP_4:8;
hence (Product f) " = Product ((Rev f) " ) by A1, GROUP_1:12; :: thesis: verum