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

end;

then x / y in Nucl_r Q by Def24;
hence x / y in Nucl Q by Th12, A9, A10; :: thesis: verum