let i be Element of 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 Th12, FINSEQOP:36
.= (a1 * R) + (a2 * R) by FUNCOP_1:31 ; :: thesis: verum