let G be Group; 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; 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 S1[ 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:
S1[ 0 ]
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let F be
FinSequence of
G;
( 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 ) )
;
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
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
;
verum
end;
A20:
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A3);
let F be FinSequence of G; ( ( 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
; h * (Product F) = (Product F) * h
len F is Nat
;
hence
h * (Product F) = (Product F) * h
by A20, A21; verum