let G be Group; :: thesis: for h being Element of G
for F being FinSequence of G st ( for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ) holds
h * (Product F) = (Product F) * h
let h be Element of G; :: thesis: for F being FinSequence of G st ( for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ) holds
h * (Product F) = (Product F) * h
defpred S₁[ Nat] means for F being FinSequence of G st len F = $1 & ( for i being Nat st i in dom F holds
h * (F /. i) = (F /. i) * h ) holds
h * (Product F) = (Product F) * h;
A1: S₁[ 0 ]

proof

let F be FinSequence of G; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds
h * (F /. i) = (F /. i) * h ) implies h * (Product F) = (Product F) * h )
assume ( len F = 0 & ( for i being Nat st i in dom F holds
h * (F /. i) = (F /. i) * h ) ) ; :: thesis: h * (Product F) = (Product F) * h
then F = <*> ([#] G) ;
then A2: Product F = 1_ G by GROUP_4:8;
hence h * (Product F) = h by GROUP_1:def 4
.= (Product F) * h by A2, GROUP_1:def 4 ;
:: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let F be FinSequence of G; :: thesis: ( len F = k + 1 & ( for i being Nat st i in dom F holds
h * (F /. i) = (F /. i) * h ) implies h * (Product F) = (Product F) * h )
assume A5: ( len F = k + 1 & ( for i being Nat st i in dom F holds
h * (F /. i) = (F /. i) * h ) ) ; :: thesis: h * (Product F) = (Product F) * h
reconsider g = F /. (k + 1) as Element of G ;
reconsider F0 = F | k as FinSequence of G ;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A6: k + 1 in dom F by A5, FINSEQ_1:def 3;
then A7: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
A8: k <= len F by A5, XREAL_1:31;
then A9: len F0 = k by FINSEQ_1:17;
A11: Seg k c= Seg (k + 1) by XREAL_1:31, FINSEQ_1:5;
A12: dom F0 = Seg k by A8, FINSEQ_1:17;
A13: dom F = Seg (k + 1) by A5, FINSEQ_1:def 3;
A14: for i being Nat st i in dom F0 holds
h * (F0 /. i) = (F0 /. i) * h

proof

let i be Nat; :: thesis: ( i in dom F0 implies h * (F0 /. i) = (F0 /. i) * h )
assume A15: i in dom F0 ; :: thesis: h * (F0 /. i) = (F0 /. i) * h
then F0 /. i = F /. i by PARTFUN1:80;
hence h * (F0 /. i) = (F0 /. i) * h by A5, A11, A12, A13, A15; :: thesis: verum

end;

A19: Product F = Product (F0 ^ <*g*>) by A5, A7, FINSEQ_3:55
.= (Product F0) * g by GROUP_4:6 ;
hence h * (Product F) = (h * (Product F0)) * g by GROUP_1:def 3
.= ((Product F0) * h) * g by A4, A9, A14
.= (Product F0) * (h * g) by GROUP_1:def 3
.= (Product F0) * (g * h) by A5, A6
.= (Product F) * h by A19, GROUP_1:def 3 ;
:: thesis: verum

end;

A20: for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A3);
let F be FinSequence of G; :: thesis: ( ( for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ) implies h * (Product F) = (Product F) * h )
assume A21: for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ; :: thesis: h * (Product F) = (Product F) * h
len F is Nat ;
hence h * (Product F) = (Product F) * h by A20, A21; :: thesis: verum