let i be Nat; :: thesis: for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
let K be non empty left_zeroed right_zeroed addLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
let R be Element of i -tuples_on the carrier of K; :: thesis: R + (i |-> (0. K)) = R
( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
hence R + (i |-> (0. K)) = R by FINSEQOP:56; :: thesis: verum