let i be Nat; :: thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
let R be Element of i -tuples_on the carrier of K; :: thesis: ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
thus R + (i |-> (0. K)) = R by Lm2; :: thesis: R = (i |-> (0. K)) + R
hence R = (i |-> (0. K)) + R by FINSEQOP:33; :: thesis: verum