let L be non empty multMagma ; :: thesis: for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
let a be Element of L; :: thesis: for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
let p, q be FinSequence of the carrier of L; :: thesis: (p ^ q) * a = (p * a) ^ (q * a)
A1: dom ((p ^ q) * a) = dom (p ^ q) by Def2;
A2: dom (q * a) = dom q by Def2;
then A3: len (q * a) = len q by FINSEQ_3:29;
A4: dom (p * a) = dom p by Def2;
then A5: len (p * a) = len p by FINSEQ_3:29;

A6: now :: thesis: for i being Nat st i in dom ((p ^ q) * a) holds
((p ^ q) * a) /. i = ((p * a) ^ (q * a)) /. i

let i be Nat; :: thesis: ( i in dom ((p ^ q) * a) implies ((p ^ q) * a) /. b₁ = ((p * a) ^ (q * a)) /. b₁ )
assume A7: i in dom ((p ^ q) * a) ; :: thesis: ((p ^ q) * a) /. b₁ = ((p * a) ^ (q * a)) /. b₁

per cases ( i in dom p or ex n being Nat st
( n in dom q & i = (len p) + n ) ) by A1, A7, FINSEQ_1:25;

suppose A8: i in dom p ; :: thesis: ((p ^ q) * a) /. b₁ = ((p * a) ^ (q * a)) /. b₁

thus ((p ^ q) * a) /. i = ((p ^ q) /. i) * a by A1, A7, Def2
.= (p /. i) * a by A8, FINSEQ_4:68
.= (p * a) /. i by A8, Def2
.= ((p * a) ^ (q * a)) /. i by A4, A8, FINSEQ_4:68 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom q & i = (len p) + n ) ; :: thesis: ((p ^ q) * a) /. b₁ = ((p * a) ^ (q * a)) /. b₁

then consider n being Nat such that
A9: n in dom q and
A10: i = (len p) + n ;
thus ((p ^ q) * a) /. i = ((p ^ q) /. i) * a by A1, A7, Def2
.= (q /. n) * a by A9, A10, FINSEQ_4:69
.= (q * a) /. n by A9, Def2
.= ((p * a) ^ (q * a)) /. i by A5, A2, A9, A10, FINSEQ_4:69 ; :: thesis: verum

end;

end;

end;

len ((p * a) ^ (q * a)) = (len (p * a)) + (len (q * a)) by FINSEQ_1:22
.= len (p ^ q) by A5, A3, FINSEQ_1:22 ;
then dom ((p ^ q) * a) = dom ((p * a) ^ (q * a)) by A1, FINSEQ_3:29;
hence (p ^ q) * a = (p * a) ^ (q * a) by A6, FINSEQ_5:12; :: thesis: verum