let G be Group; for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
defpred S1[ Nat] means for F, F1, F2 being FinSequence of G st len F = $1 & len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2);
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,
F1,
F2 be
FinSequence of
G;
( len F = k + 1 & len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) implies Product F = (Product F1) * (Product F2) )
assume A5:
(
len F = k + 1 &
len F = len F1 &
len F = len F2 & ( for
i,
j being
Nat st
i in dom F &
j in dom F &
i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for
k being
Nat st
k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) )
;
Product F = (Product F1) * (Product F2)
reconsider g =
F /. (k + 1) as
Element of
G ;
reconsider h =
F1 /. (k + 1) as
Element of
G ;
reconsider i =
F2 /. (k + 1) as
Element of
G ;
reconsider F0 =
F | k as
FinSequence of
G ;
reconsider F10 =
F1 | k as
FinSequence of
G ;
reconsider F20 =
F2 | k as
FinSequence of
G ;
A6:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A7:
k + 1
in dom F
by A5, FINSEQ_1:def 3;
then A8:
F /. (k + 1) = F . (k + 1)
by PARTFUN1:def 6;
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then
k + 1
in dom F1
by A5, FINSEQ_1:def 3;
then A9:
F1 /. (k + 1) = F1 . (k + 1)
by PARTFUN1:def 6;
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then
k + 1
in dom F2
by A5, FINSEQ_1:def 3;
then A10:
F2 /. (k + 1) = F2 . (k + 1)
by PARTFUN1:def 6;
A12:
(
k <= len F &
k <= len F1 &
k <= len F2 )
by A5, XREAL_1:31;
then A13:
(
len F0 = k &
len F10 = k &
len F20 = k )
by FINSEQ_1:17;
A15:
Seg k c= Seg (k + 1)
by FINSEQ_1:5, XREAL_1:31;
A16:
dom F0 = Seg k
by A12, FINSEQ_1:17;
then A17:
dom F10 = dom F0
by A12, FINSEQ_1:17;
A18:
dom F20 = dom F0
by A12, A16, FINSEQ_1:17;
A19:
dom F = Seg (k + 1)
by A5, FINSEQ_1:def 3;
A22:
for
i,
j being
Nat st
i in dom F0 &
j in dom F0 &
i <> j holds
(F10 /. i) * (F20 /. j) = (F20 /. j) * (F10 /. i)
proof
let i,
j be
Nat;
( i in dom F0 & j in dom F0 & i <> j implies (F10 /. i) * (F20 /. j) = (F20 /. j) * (F10 /. i) )
assume A23:
(
i in dom F0 &
j in dom F0 &
i <> j )
;
(F10 /. i) * (F20 /. j) = (F20 /. j) * (F10 /. i)
then A27:
F10 /. i = F1 /. i
by A17, PARTFUN1:80;
hence (F10 /. i) * (F20 /. j) =
(F1 /. i) * (F2 /. j)
by A18, A23, PARTFUN1:80
.=
(F2 /. j) * (F1 /. i)
by A5, A15, A16, A19, A23
.=
(F20 /. j) * (F10 /. i)
by A18, A23, A27, PARTFUN1:80
;
verum
end;
A29:
for
k being
Nat st
k in dom F0 holds
F0 . k = (F10 /. k) * (F20 /. k)
A36:
for
i being
Nat st
i in dom F20 holds
h * (F20 /. i) = (F20 /. i) * h
proof
let i be
Nat;
( i in dom F20 implies h * (F20 /. i) = (F20 /. i) * h )
assume A37:
i in dom F20
;
h * (F20 /. i) = (F20 /. i) * h
then A40:
F20 /. i = F2 /. i
by PARTFUN1:80;
dom F20 = Seg k
by A12, FINSEQ_1:17;
then A41:
( 1
<= i &
i <= k )
by A37, FINSEQ_1:1;
k + 0 < k + 1
by XREAL_1:8;
hence
h * (F20 /. i) = (F20 /. i) * h
by A5, A6, A15, A16, A18, A19, A37, A40, A41;
verum
end;
A43:
g =
F . (k + 1)
by A7, PARTFUN1:def 6
.=
h * i
by A5, A7
;
A44:
Product F1 =
Product (F10 ^ <*h*>)
by A5, A9, FINSEQ_3:55
.=
(Product F10) * h
by GROUP_4:6
;
A45:
Product F2 =
Product (F20 ^ <*i*>)
by A5, A10, FINSEQ_3:55
.=
(Product F20) * i
by GROUP_4:6
;
thus Product F =
Product (F0 ^ <*g*>)
by A5, A8, FINSEQ_3:55
.=
(Product F0) * g
by GROUP_4:6
.=
((Product F10) * (Product F20)) * (h * i)
by A4, A13, A22, A29, A43
.=
(((Product F10) * (Product F20)) * h) * i
by GROUP_1:def 3
.=
((Product F10) * ((Product F20) * h)) * i
by GROUP_1:def 3
.=
((Product F10) * (h * (Product F20))) * i
by A36, Th46
.=
(((Product F10) * h) * (Product F20)) * i
by GROUP_1:def 3
.=
(Product F1) * (Product F2)
by A44, A45, GROUP_1:def 3
;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A3);
hence
for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
; verum