let K be non empty commutative multMagma ; :: thesis: for p, q being FinSequence of the carrier of K holds mlt p,q = mlt q,p
let p, q be FinSequence of the carrier of K; :: thesis: mlt p,q = mlt q,p
reconsider r = mlt p,q as FinSequence of the carrier of K ;
reconsider s = mlt q,p as FinSequence of the carrier of K ;
A1: ( len r = min (len p),(len q) & len s = min (len q),(len p) ) by FINSEQ_2:85;
reconsider k = min (len p),(len q) as Element of NAT by XXREAL_0:15;
A2: ( dom r = Seg k & dom s = Seg k ) by A1, FINSEQ_1:def 3;
( min (len p),(len q) <= len p & min (len p),(len q) <= len q ) by XXREAL_0:17;
then ( Seg k c= Seg (len p) & Seg k c= Seg (len q) ) by FINSEQ_1:7;
then A3: ( Seg k c= dom p & Seg k c= dom q ) by FINSEQ_1:def 3;
X: dom r = Seg k by A1, FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom r implies r . i = s . i )
assume A4: i in dom r ; :: thesis: r . i = s . i
then reconsider d1 = p . i, d2 = q . i as Element of K by A3, X, FINSEQ_2:13;
thus r . i = d1 * d2 by A4, FUNCOP_1:28
.= d2 * d1
.= s . i by A2, A4, FUNCOP_1:28 ; :: thesis: verum

end;

hence mlt p,q = mlt q,p by A1, FINSEQ_2:10; :: thesis: verum