let i be Nat; :: thesis: for K being non empty associative commutative multMagma
for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
let K be non empty associative commutative multMagma ; :: thesis: for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
let a1, a2 be Element of K; :: thesis: mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
thus mlt ((i |-> a1),(i |-> a2)) = a1 * (i |-> a2) by Th66
.= i |-> (a1 * a2) by Th53 ; :: thesis: verum