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: now :: thesis: for F being FinSequence of the carrier of G
for b being Element of G st S₁[F] holds
S₁[F ^ <*b*>]

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 A2: S₁[F] ; :: thesis: S₁[F ^ <*b*>]
Product ((F ^ <*b*>) |^ a) = Product ((F |^ a) ^ (<*b*> |^ a)) by Th9
.= ((Product F) |^ a) * (Product (<*b*> |^ a)) by A2, GROUP_4:5
.= ((Product F) |^ a) * (Product <*(b |^ a)*>) by Th11
.= ((Product F) |^ a) * (b |^ a) by FINSOP_1:11
.= ((Product F) * b) |^ a by GROUP_3:23
.= (Product (F ^ <*b*>)) |^ a by GROUP_4:6 ;
hence S₁[F ^ <*b*>] ; :: thesis: verum

end;

A3: 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 Th10
.= 1_ G by GROUP_4:8
.= (1_ G) |^ a by GROUP_3:17
.= (Product (<*> the carrier of G)) |^ a by GROUP_4:8 ; :: thesis: verum

end;

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