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) = dom p by Def2;
then A2: len (a * p) = len p by FINSEQ_3:31;
A3: dom (a * q) = dom q by Def2;
then A4: len (a * q) = len q by FINSEQ_3:31;
A5: len ((a * p) ^ (a * q)) = (len (a * p)) + (len (a * q)) by FINSEQ_1:35
.= len (p ^ q) by A2, A4, FINSEQ_1:35 ;
A6: dom (a * (p ^ q)) = dom (p ^ q) by Def2;
then A7: dom (a * (p ^ q)) = dom ((a * p) ^ (a * q)) by A5, FINSEQ_3:31;

now

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

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

thus (a * (p ^ q)) /. i = a * ((p ^ q) /. i) by A6, A8, Def2
.= a * (p /. i) by A9, FINSEQ_4:83
.= (a * p) /. i by A9, Def2
.= ((a * p) ^ (a * q)) /. i by A1, A9, 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
A10: ( n in dom q & i = (len p) + n ) ;
thus (a * (p ^ q)) /. i = a * ((p ^ q) /. i) by A6, A8, Def2
.= a * (q /. n) by A10, FINSEQ_4:84
.= (a * q) /. n by A10, Def2
.= ((a * p) ^ (a * q)) /. i by A2, A3, A10, FINSEQ_4:84 ; :: thesis: verum

end;

end;

end;

hence a * (p ^ q) = (a * p) ^ (a * q) by A7, FINSEQ_5:13; :: thesis: verum