let R be non empty commutative multMagma ; :: thesis: for a being Element of R
for p being FinSequence of the carrier of R holds p * a = a * p
let a be Element of R; :: thesis: for p being FinSequence of the carrier of R holds p * a = a * p
let p be FinSequence of the carrier of R; :: thesis: p * a = a * p
set pa = p * a;
set ap = a * p;
A1: dom (p * a) = dom p by POLYNOM1:def 2;
A2: dom (a * p) = dom p by POLYNOM1:def 1;

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

let i be Nat; :: thesis: ( i in dom (p * a) implies (p * a) /. i = (a * p) /. i )
assume A3: i in dom (p * a) ; :: thesis: (p * a) /. i = (a * p) /. i
thus (p * a) /. i = (p /. i) * a by A1, A3, POLYNOM1:def 2
.= (a * p) /. i by A1, A3, POLYNOM1:def 1 ; :: thesis: verum

end;

hence p * a = a * p by A1, A2, FINSEQ_5:12; :: thesis: verum