let i be Element of 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:21
.= a * R by FINSEQOP:23 ; :: thesis: mlt R,(i |-> a) = a * R
hence mlt R,(i |-> a) = a * R by FINSEQOP:34; :: thesis: verum