let i be Nat; :: thesis: for K being non empty distributive doubleLoopStr
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)
let K be non empty distributive doubleLoopStr ; :: 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 * R) + (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 * R) + (a2 * R)
let R be Element of i -tuples_on the carrier of K; :: thesis: (a1 + a2) * R = (a1 * R) + (a2 * R)
thus (a1 + a2) * R = ( the addF of K .: (( the multF of K [;] (a1,(id the carrier of K))),( the multF of K [;] (a2,(id the carrier of K))))) * R by Th10, FINSEQOP:35
.= (a1 * R) + (a2 * R) by FUNCOP_1:25 ; :: thesis: verum