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 * (((x \ y) * z) * w) = (x * ((x \ y) * z)) * w by A3, Def22
.= ((x * (x \ y)) * z) * w by A3, Def22
.= (x * (x \ y)) * (z * w) by A6, Def22
.= x * ((x \ y) * (z * w)) by A3, Def22 ;
hence ((x \ y) * z) * w = (x \ y) * (z * w) by Th1; :: 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) * x) * (x \ y)) * w
.= ((z / x) * (x * (x \ y))) * w by A4, Def23
.= (z / x) * ((x * (x \ y)) * w) by A7, Def23
.= (z / x) * (x * ((x \ y) * w)) by A3, Def22
.= ((z / x) * x) * ((x \ y) * w) by A4, Def23
.= z * ((x \ y) * w) ;
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) * x)) * (x \ y)
.= ((z * (w / x)) * x) * (x \ y) by A5, Def24
.= (z * (w / x)) * (x * (x \ y)) by A4, Def23
.= z * ((w / x) * (x * (x \ y))) by A8, Def24
.= z * (((w / x) * x) * (x \ y)) by A4, Def23
.= z * (w * (x \ y)) ;
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