let Q be multLoop; :: thesis: 1. Q in Nucl_l Q
for y, z being Element of Q holds ((1. Q) * y) * z = (1. Q) * (y * z) ;
hence 1. Q in Nucl_l Q by Def22; :: thesis: verum