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