let G be Group; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: (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 :: thesis: 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; :: thesis: ( k in dom (F1 ^ F2) implies ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) )
assume A5: k in dom (F1 ^ F2) ; :: thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))

now :: thesis: ((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 ; :: thesis: ((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; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom F2 & k = (len F1) + n ) ; :: thesis: ((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; :: thesis: verum

end;

end;

end;

hence ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) ; :: thesis: 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; :: thesis: verum