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:71;
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:5;
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:5;
then A4: Seg k c= dom p by FINSEQ_1:def 3;
A5: len s = min ((len q),(len p)) by FINSEQ_2:71;
then A6: dom s = Seg k by FINSEQ_1:def 3;
A7: dom r = Seg k by A1, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom r holds
r . i = s . i
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:11;
thus r . i = d1 * d2 by A8, FUNCOP_1:22
.= d2 * d1
.= s . i by A7, A6, A8, FUNCOP_1:22 ; :: thesis: verum
end;
hence mlt (p,q) = mlt (q,p) by A1, A5, FINSEQ_2:9; :: thesis: verum