let G be Group; :: thesis: for a being Element of G
for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
let a be Element of G; :: thesis: for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
let F1, F2 be FinSequence of the carrier of G; :: thesis: (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
A1: now :: thesis: for k being Nat st k in dom (F1 |^ a) holds
(F1 |^ a) . k = ((F1 ^ F2) |^ a) . k
let k be Nat; :: thesis: ( k in dom (F1 |^ a) implies (F1 |^ a) . k = ((F1 ^ F2) |^ a) . k )
assume k in dom (F1 |^ a) ; :: thesis: (F1 |^ a) . k = ((F1 ^ F2) |^ a) . k
then k in Seg (len (F1 |^ a)) by FINSEQ_1:def 3;
then k in Seg (len F1) by Def1;
then A2: k in dom F1 by FINSEQ_1:def 3;
then A3: ( F1 /. k = (F1 ^ F2) /. k & k in dom (F1 ^ F2) ) by FINSEQ_3:22, FINSEQ_4:68;
thus (F1 |^ a) . k = (F1 /. k) |^ a by A2, Def1
.= ((F1 ^ F2) |^ a) . k by A3, Def1 ; :: thesis: verum
end;
A4: now :: thesis: for k being Nat st k in dom (F2 |^ a) holds
((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = (F2 |^ a) . k
let k be Nat; :: thesis: ( k in dom (F2 |^ a) implies ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = (F2 |^ a) . k )
assume A5: k in dom (F2 |^ a) ; :: thesis: ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = (F2 |^ a) . k
len F2 = len (F2 |^ a) by Def1;
then A6: k in dom F2 by A5, FINSEQ_3:29;
then (len F1) + k in dom (F1 ^ F2) by FINSEQ_1:28;
then (len (F1 |^ a)) + k in dom (F1 ^ F2) by Def1;
hence ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = ((F1 ^ F2) /. ((len (F1 |^ a)) + k)) |^ a by Def1
.= ((F1 ^ F2) /. ((len F1) + k)) |^ a by Def1
.= (F2 /. k) |^ a by A6, FINSEQ_4:69
.= (F2 |^ a) . k by A6, Def1 ;
:: thesis: verum
end;
(len (F1 |^ a)) + (len (F2 |^ a)) = (len F1) + (len (F2 |^ a)) by Def1
.= (len F1) + (len F2) by Def1
.= len (F1 ^ F2) by FINSEQ_1:22
.= len ((F1 ^ F2) |^ a) by Def1 ;
hence (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a by A1, A4, FINSEQ_3:38; :: thesis: verum