let i be Element of NAT ; :: thesis: for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
let R be Element of i -tuples_on the carrier of K; :: thesis: (0. K) * R = i |-> (0. K)
A1: rng R c= the carrier of K by FINSEQ_1:def 4;
A2: the addF of K is having_an_inverseOp by Th17;
A3: ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th9, Th10;
thus (0. K) * R = the multF of K [;] (0. K),((id the carrier of K) * R) by FUNCOP_1:44
.= the multF of K [;] (0. K),R by A1, RELAT_1:79
.= i |-> (0. K) by A3, A2, Th12, FINSEQOP:80 ; :: thesis: verum