let G be Group; :: thesis: for a being Element of G holds Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = a |^ (Sum (<*> INT ))
let a be Element of G; :: thesis: Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = a |^ (Sum (<*> INT ))
A1: (len (<*> INT )) |-> a = 0 |-> a
.= <*> the carrier of G ;
(<*> the carrier of G) |^ (<*> INT ) = <*> the carrier of G by GROUP_4:27;
then Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = 1_ G by A1, GROUP_4:11
.= a |^ (Sum (<*> INT )) by Th22, GROUP_1:43 ;
hence Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = a |^ (Sum (<*> INT )) ; :: thesis: verum