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

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

let i be Nat; :: thesis: ( i in dom (a * (p ^ q)) implies (a * (p ^ q)) /. b₁ = ((a * p) ^ (a * q)) /. b₁ )
assume A7: i in dom (a * (p ^ q)) ; :: thesis: (a * (p ^ q)) /. b₁ = ((a * p) ^ (a * q)) /. 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: (a * (p ^ q)) /. b₁ = ((a * p) ^ (a * q)) /. b₁

thus (a * (p ^ q)) /. i = a * ((p ^ q) /. i) by A1, A7, Def1
.= a * (p /. i) by A8, FINSEQ_4:68
.= (a * p) /. i by A8, Def1
.= ((a * p) ^ (a * q)) /. 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: (a * (p ^ q)) /. b₁ = ((a * p) ^ (a * q)) /. b₁

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

end;

end;

end;

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