let i be Nat; :: thesis: for K being non empty associative multMagma
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let K be non empty associative multMagma ; :: thesis: for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let a1, a2 be Element of K; :: thesis: for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let R be Element of i -tuples_on the carrier of K; :: thesis: (a1 * a2) * R = a1 * (a2 * R)
set F = the multF of K;
set f = id the carrier of K;
thus (a1 * a2) * R = ( the multF of K [;] (a1,( the multF of K [;] (a2,(id the carrier of K))))) * R by FUNCOP_1:62
.= (( the multF of K [;] (a1,(id the carrier of K))) * ( the multF of K [;] (a2,(id the carrier of K)))) * R by FUNCOP_1:55
.= a1 * (a2 * R) by RELAT_1:36 ; :: thesis: verum