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))
(<*> the carrier of G) |^ (<*> INT) = <*> the carrier of G by GROUP_4:21;
then Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = 1_ G by GROUP_4:8
.= a |^ (Sum (<*> INT)) by Th3, GROUP_1:25 ;
hence Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT)) ; :: thesis: verum