let i be Nat; :: thesis: for K being non empty multMagma
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
let K be non empty multMagma ; :: thesis: for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
let a1, a2 be Element of K; :: thesis: a1 * (i |-> a2) = i |-> (a1 * a2)
thus a1 * (i |-> a2) = i |-> (( the multF of K [;] (a1,(id the carrier of K))) . a2) by FINSEQOP:16
.= i |-> (a1 * a2) by Th48 ; :: thesis: verum