theorem :: STRUCT_0:4

for S being non empty ZeroStr holds the carrier of S = {(0. S)} \/ (NonZero S) by XBOOLE_1:45;