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_{1}[ FinSequence of the carrier of G] means Product ($1 |^ a) = (Product $1) |^ a;

_{1}[ <*> the carrier of G]
_{1}[F]
from FINSEQ_2:sch 2(A3, A1);

hence Product (F |^ a) = (Product F) |^ a ; :: thesis: verum

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

A1: now :: thesis: for F being FinSequence of the carrier of G

for b being Element of G st S_{1}[F] holds

S_{1}[F ^ <*b*>]

A3:
Sfor b being Element of G st S

S

let F be FinSequence of the carrier of G; :: thesis: for b being Element of G st S_{1}[F] holds

S_{1}[F ^ <*b*>]

let b be Element of G; :: thesis: ( S_{1}[F] implies S_{1}[F ^ <*b*>] )

assume A2: S_{1}[F]
; :: thesis: S_{1}[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_{1}[F ^ <*b*>]
; :: thesis: verum

end;S

let b be Element of G; :: thesis: ( S

assume A2: S

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

proof

for F being FinSequence of the carrier of G holds S
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;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

hence Product (F |^ a) = (Product F) |^ a ; :: thesis: verum