let Q be multLoop; :: thesis: for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x * y in Nucl Q
let x, y be Element of Q; :: thesis: ( x in Nucl Q & y in Nucl Q implies x * y in Nucl Q )
assume that
A1: x in Nucl Q and
A2: y in Nucl Q ; :: thesis: x * y in Nucl Q
A3: x in Nucl_l Q by Th12, A1;
A4: x in Nucl_m Q by Th12, A1;
A5: x in Nucl_r Q by Th12, A1;
A6: y in Nucl_l Q by Th12, A2;
A7: y in Nucl_m Q by Th12, A2;
A8: y in Nucl_r Q by Th12, A2;
for z, w being Element of Q holds ((x * y) * z) * w = (x * y) * (z * w)
proof
let z, w be Element of Q; :: thesis: ((x * y) * z) * w = (x * y) * (z * w)
((x * y) * z) * w = (x * (y * z)) * w by A3, Def22
.= x * ((y * z) * w) by A3, Def22
.= x * (y * (z * w)) by A6, Def22
.= (x * y) * (z * w) by A3, Def22 ;
hence ((x * y) * z) * w = (x * y) * (z * w) ; :: thesis: verum
end;
then A9: x * y in Nucl_l Q by Def22;
for z, w being Element of Q holds (z * (x * y)) * w = z * ((x * y) * w)
proof
let z, w be Element of Q; :: thesis: (z * (x * y)) * w = z * ((x * y) * w)
(z * (x * y)) * w = ((z * x) * y) * w by A4, Def23
.= (z * x) * (y * w) by A7, Def23
.= z * (x * (y * w)) by A4, Def23
.= z * ((x * y) * w) by A7, Def23 ;
hence (z * (x * y)) * w = z * ((x * y) * w) ; :: thesis: verum
end;
then A10: x * y in Nucl_m Q by Def23;
for z, w being Element of Q holds (z * w) * (x * y) = z * (w * (x * y))
proof
let z, w be Element of Q; :: thesis: (z * w) * (x * y) = z * (w * (x * y))
(z * w) * (x * y) = ((z * w) * x) * y by A8, Def24
.= (z * (w * x)) * y by A5, Def24
.= z * ((w * x) * y) by A8, Def24
.= z * (w * (x * y)) by A8, Def24 ;
hence (z * w) * (x * y) = z * (w * (x * y)) ; :: thesis: verum
end;
then x * y in Nucl_r Q by Def24;
hence x * y in Nucl Q by Th12, A9, A10; :: thesis: verum