let V be non empty addLoopStr ; :: thesis: for v being Element of V holds (Z_ZeroLC V) . v = 0
let v be Element of V; :: thesis: (Z_ZeroLC V) . v = 0
( Carrier (Z_ZeroLC V) = {} & not v in {} ) by Def20;
hence (Z_ZeroLC V) . v = 0 ; :: thesis: verum