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 A1: ( len F1 = len I1 & len F2 = len I2 ) ; :: thesis: (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
set q = F1 |^ I1;
set r = F2 |^ I2;
A2: len ((F1 |^ I1) ^ (F2 |^ I2)) = (len (F1 |^ I1)) + (len (F2 |^ I2)) by FINSEQ_1:35
.= (len F1) + (len (F2 |^ I2)) by Def4
.= (len F1) + (len F2) by Def4
.= len (F1 ^ F2) by FINSEQ_1:35 ;
len (F1 ^ F2) = (len F1) + (len F2) by FINSEQ_1:35
.= len (I1 ^ I2) by A1, FINSEQ_1:35 ;
then A3: dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:31;

now

let k be Element of NAT ; :: thesis: ( k in dom (F1 ^ F2) implies ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) )
assume A4: k in dom (F1 ^ F2) ; :: thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))

now

per cases ( k in dom F1 or ex n being Nat st
( n in dom F2 & k = (len F1) + n ) ) by A4, FINSEQ_1:38;

suppose A5: k in dom F1 ; :: thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))

then A6: k in dom I1 by A1, FINSEQ_3:31;
then A7: I1 /. k = I1 . k by PARTFUN1:def 8;
A8: (I1 ^ I2) . k = (I1 ^ I2) /. k by A3, A4, PARTFUN1:def 8;
len (F1 |^ I1) = len F1 by Def4;
then k in dom (F1 |^ I1) by A5, FINSEQ_3:31;
then A9: ((F1 |^ I1) ^ (F2 |^ I2)) . k = (F1 |^ I1) . k by FINSEQ_1:def 7
.= (F1 /. k) |^ (@ (I1 /. k)) by A5, Def4 ;
F1 /. k = F1 . k by A5, PARTFUN1:def 8
.= (F1 ^ F2) . k by A5, FINSEQ_1:def 7
.= (F1 ^ F2) /. k by A4, PARTFUN1:def 8 ;
hence ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) by A6, A7, A8, 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 Element of NAT such that
A10: n in dom F2 and
A11: k = (len F1) + n ;
A12: ( len (F2 |^ I2) = len F2 & len (F1 |^ I1) = len F1 ) by Def4;
then A13: ( n in dom (F2 |^ I2) & n in dom I2 ) by A1, A10, FINSEQ_3:31;
then A14: ( ((F1 |^ I1) ^ (F2 |^ I2)) . k = (F2 |^ I2) . n & (I1 ^ I2) . k = I2 . n & (F1 ^ F2) . k = F2 . n & n in dom F2 & (F1 ^ F2) . k = (F1 ^ F2) /. k & F2 . n = F2 /. n ) by A1, A4, A10, A11, A12, FINSEQ_1:def 7, PARTFUN1:def 8;
A15: (I1 ^ I2) /. k = (I1 ^ I2) . k by A3, A4, PARTFUN1:def 8;
I2 /. n = I2 . n by A13, PARTFUN1:def 8;
hence ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) by A14, A15, Def4; :: thesis: verum

end;

end;

end;

hence ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) ; :: thesis: verum

end;

hence (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) by A2, Def4; :: thesis: verum