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