let G be Group; :: thesis: for a being Element of G
for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let a be Element of G; :: thesis: for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let I be FinSequence of INT ; :: thesis: for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let w be Element of INT ; :: thesis: ( Product (((len I) |-> a) |^ I) = a |^ (Sum I) implies Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>)) )
assume A1: Product (((len I) |-> a) |^ I) = a |^ (Sum I) ; :: thesis: Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
A2: len ((len I) |-> a) = len I by CARD_1:def 7;
A3: len <*a*> = 1 by FINSEQ_1:40
.= len <*w*> by FINSEQ_1:40 ;
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = Product ((((len I) + 1) |-> a) |^ (I ^ <*w*>)) by FINSEQ_2:16
.= Product ((((len I) |-> a) ^ <*a*>) |^ (I ^ <*w*>)) by FINSEQ_2:60
.= Product ((((len I) |-> a) |^ I) ^ (<*a*> |^ <*w*>)) by A2, A3, GROUP_4:19
.= (Product (((len I) |-> a) |^ I)) * (Product (<*a*> |^ <*(@ (@ w))*>)) by GROUP_4:5
.= (Product (((len I) |-> a) |^ I)) * (Product <*(a |^ (@ w))*>) by GROUP_4:22
.= (a |^ (Sum I)) * (a |^ (@ w)) by A1, FINSOP_1:11
.= a |^ ((Sum I) + (@ w)) by GROUP_1:33
.= a |^ (Sum (I ^ <*w*>)) by RVSUM_1:74 ;
hence Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>)) ; :: thesis: verum