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