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