let G be Group; for F1, F2 being FinSequence of the carrier of G
for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
let F1, F2 be FinSequence of the carrier of G; for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
let I1, I2 be FinSequence of INT ; ( len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) )
assume that
A1:
len F1 = len I1
and
A2:
len F2 = len I2
; (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
set r = F2 |^ I2;
set q = F1 |^ I1;
len (F1 ^ F2) =
(len F1) + (len F2)
by FINSEQ_1:22
.=
len (I1 ^ I2)
by A1, A2, FINSEQ_1:22
;
then A3:
dom (F1 ^ F2) = dom (I1 ^ I2)
by FINSEQ_3:29;
A4:
now for k being Nat st k in dom (F1 ^ F2) holds
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))let k be
Nat;
( k in dom (F1 ^ F2) implies ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) )assume A5:
k in dom (F1 ^ F2)
;
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))now ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))per cases
( k in dom F1 or ex n being Nat st
( n in dom F2 & k = (len F1) + n ) )
by A5, FINSEQ_1:25;
suppose A6:
k in dom F1
;
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
len (F1 |^ I1) = len F1
by Def3;
then
k in dom (F1 |^ I1)
by A6, FINSEQ_3:29;
then A7:
((F1 |^ I1) ^ (F2 |^ I2)) . k =
(F1 |^ I1) . k
by FINSEQ_1:def 7
.=
(F1 /. k) |^ (@ (I1 /. k))
by A6, Def3
;
A8:
(I1 ^ I2) . k = (I1 ^ I2) /. k
by A3, A5, PARTFUN1:def 6;
A9:
F1 /. k =
F1 . k
by A6, PARTFUN1:def 6
.=
(F1 ^ F2) . k
by A6, FINSEQ_1:def 7
.=
(F1 ^ F2) /. k
by A5, PARTFUN1:def 6
;
A10:
k in dom I1
by A1, A6, FINSEQ_3:29;
then
I1 /. k = I1 . k
by PARTFUN1:def 6;
hence
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
by A10, A8, A7, A9, FINSEQ_1:def 7;
verum end; suppose
ex
n being
Nat st
(
n in dom F2 &
k = (len F1) + n )
;
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))then consider n being
Nat such that A11:
n in dom F2
and A12:
k = (len F1) + n
;
A13:
(
(F1 ^ F2) . k = F2 . n &
F2 . n = F2 /. n )
by A11, A12, FINSEQ_1:def 7, PARTFUN1:def 6;
A14:
len (F1 |^ I1) = len F1
by Def3;
len (F2 |^ I2) = len F2
by Def3;
then
n in dom (F2 |^ I2)
by A11, FINSEQ_3:29;
then A15:
((F1 |^ I1) ^ (F2 |^ I2)) . k = (F2 |^ I2) . n
by A12, A14, FINSEQ_1:def 7;
A16:
(
(F1 ^ F2) . k = (F1 ^ F2) /. k &
(I1 ^ I2) /. k = (I1 ^ I2) . k )
by A3, A5, PARTFUN1:def 6;
A17:
n in dom I2
by A2, A11, FINSEQ_3:29;
then A18:
I2 /. n = I2 . n
by PARTFUN1:def 6;
(I1 ^ I2) . k = I2 . n
by A1, A12, A17, FINSEQ_1:def 7;
hence
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
by A11, A15, A13, A16, A18, Def3;
verum end; end; end; hence
((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
;
verum end;
len ((F1 |^ I1) ^ (F2 |^ I2)) =
(len (F1 |^ I1)) + (len (F2 |^ I2))
by FINSEQ_1:22
.=
(len F1) + (len (F2 |^ I2))
by Def3
.=
(len F1) + (len F2)
by Def3
.=
len (F1 ^ F2)
by FINSEQ_1:22
;
hence
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
by A4, Def3; verum