let K be non empty addLoopStr ; :: thesis: for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K
let R be Element of 0 -tuples_on the carrier of K; :: thesis: Sum R = 0. K
R = <*> the carrier of K ;
hence Sum R = 0. K by RLVECT_1:43; :: thesis: verum