let i be Nat; :: thesis: for K being non empty commutative distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R
let K be non empty commutative distributive left_unital doubleLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R
let R be Element of i -tuples_on the carrier of K; :: thesis: (1. K) * R = R
A1: rng R c= the carrier of K by FINSEQ_1:def 4;
the_unity_wrt the multF of K = 1. K by Th5;
hence (1. K) * R = (id the carrier of K) * R by FINSEQOP:44
.= R by A1, RELAT_1:53 ;
:: thesis: verum