let i be Nat; :: thesis: for K being non empty associative commutative multMagma
for a being Element of K
for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let K be non empty associative commutative multMagma ; :: thesis: for a being Element of K
for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let a be Element of K; :: thesis: for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let R be Element of i -tuples_on the carrier of K; :: thesis: ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
thus mlt ((i |-> a),R) = the multF of K [;] (a,R) by FINSEQOP:20
.= a * R by FINSEQOP:22 ; :: thesis: mlt (R,(i |-> a)) = a * R
hence mlt (R,(i |-> a)) = a * R by FINSEQOP:33; :: thesis: verum