let i, j be Nat; :: thesis: for K being Field
for R1, S1 being Element of i -tuples_on the carrier of K
for R2, S2 being Element of j -tuples_on the carrier of K holds Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2)))
let K be Field; :: thesis: for R1, S1 being Element of i -tuples_on the carrier of K
for R2, S2 being Element of j -tuples_on the carrier of K holds Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2)))
let R1, S1 be Element of i -tuples_on the carrier of K; :: thesis: for R2, S2 being Element of j -tuples_on the carrier of K holds Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2)))
let R2, S2 be Element of j -tuples_on the carrier of K; :: thesis: Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2)))
mlt ((R1 ^ R2),(S1 ^ S2)) = (mlt (R1,S1)) ^ (mlt (R2,S2)) by FINSEQOP:11;
hence Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2))) by RLVECT_1:41; :: thesis: verum