let i be Nat; :: thesis: for K being non empty right_complementable distributive add-associative right_zeroed 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 distributive add-associative right_zeroed 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 Th14;
A3: ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
thus (0. K) * R = the multF of K [;] ((0. K),((id the carrier of K) * R)) by FUNCOP_1:34
.= the multF of K [;] ((0. K),R) by A1, RELAT_1:53
.= i |-> (0. K) by A3, A2, Th10, FINSEQOP:76 ; :: thesis: verum