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 S1[ 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 S1[F] holds
S1[F ^ <*b*>]
let F be FinSequence of the carrier of G; :: thesis: for b being Element of G st S1[F] holds
S1[F ^ <*b*>]
let b be Element of G; :: thesis: ( S1[F] implies S1[F ^ <*b*>] )
assume A2: S1[F] ; :: thesis: S1[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 S1[F ^ <*b*>] ; :: thesis: verum
end;
A3: S1[ <*> 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 S1[F] from FINSEQ_2:sch 2(A3, A1);
 hence Product (F |^ a) = (Product F) |^ a ; :: thesis: verum