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 ;
reconsider k = min (len p),(len q) as Element of NAT by XXREAL_0:15;
A1: len r = min (len p),(len q) by FINSEQ_2:85;
then A2: dom r = Seg k by FINSEQ_1:def 3;
min (len p),(len q) <= len q by XXREAL_0:17;
then Seg k c= Seg (len q) by FINSEQ_1:7;
then A3: Seg k c= dom q by FINSEQ_1:def 3;
min (len p),(len q) <= len p by XXREAL_0:17;
then Seg k c= Seg (len p) by FINSEQ_1:7;
then A4: Seg k c= dom p by FINSEQ_1:def 3;
A5: len s = min (len q),(len p) by FINSEQ_2:85;
then A6: dom s = Seg k by FINSEQ_1:def 3;
A7: 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 A8: i in dom r ; :: thesis: r . i = s . i
then reconsider d1 = p . i, d2 = q . i as Element of K by A4, A3, A2, FINSEQ_2:13;
thus r . i = d1 * d2 by A8, FUNCOP_1:28
.= d2 * d1
.= s . i by A7, A6, A8, FUNCOP_1:28 ; :: thesis: verum

end;

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