let G be Group; :: thesis: for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
let a be Element of G; :: thesis: for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
let F be FinSequence of the carrier of G; :: thesis: Product (F |^ a) = (Product F) |^ a
defpred S₁[ FinSequence of the carrier of G] means Product ($1 |^ a) = (Product $1) |^ a;
A1: S₁[ <*> the carrier of G]

proof

set p = <*> the carrier of G;
thus Product ((<*> the carrier of G) |^ a) = Product (<*> the carrier of G) by Th13
.= 1_ G by GROUP_4:11
.= (1_ G) |^ a by GROUP_3:22
.= (Product (<*> the carrier of G)) |^ a by GROUP_4:11 ; :: thesis: verum

end;

A2: now

let F be FinSequence of the carrier of G; :: thesis: for b being Element of G st S₁[F] holds
S₁[F ^ <*b*>]
let b be Element of G; :: thesis: ( S₁[F] implies S₁[F ^ <*b*>] )
assume A3: S₁[F] ; :: thesis: S₁[F ^ <*b*>]
thus S₁[F ^ <*b*>] :: thesis: verum

proof

thus Product ((F ^ <*b*>) |^ a) = Product ((F |^ a) ^ (<*b*> |^ a)) by Th12
.= ((Product F) |^ a) * (Product (<*b*> |^ a)) by A3, GROUP_4:8
.= ((Product F) |^ a) * (Product <*(b |^ a)*>) by Th14
.= ((Product F) |^ a) * (b |^ a) by FINSOP_1:12
.= ((Product F) * b) |^ a by GROUP_3:28
.= (Product (F ^ <*b*>)) |^ a by GROUP_4:9 ; :: thesis: verum

end;

end;

for F being FinSequence of the carrier of G holds S₁[F] from FINSEQ_2:sch 2(A1, A2);
hence Product (F |^ a) = (Product F) |^ a ; :: thesis: verum