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 Def2;
A2: dom (a * q) = dom q by Def2;
then A3: len (a * q) = len q by FINSEQ_3:31;
A4: dom (a * p) = dom p by Def2;
then A5: len (a * p) = len p by FINSEQ_3:31;

A6: now

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:38;

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, Def2
.= a * (p /. i) by A8, FINSEQ_4:83
.= (a * p) /. i by A8, Def2
.= ((a * p) ^ (a * q)) /. i by A4, A8, FINSEQ_4:83 ; :: 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, Def2
.= a * (q /. n) by A9, A10, FINSEQ_4:84
.= (a * q) /. n by A9, Def2
.= ((a * p) ^ (a * q)) /. i by A5, A2, A9, A10, FINSEQ_4:84 ; :: thesis: verum

end;

end;

end;

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