let Q be AIM multLoop; :: thesis: for x, u being Element of Q st u in Nucl Q holds
(x * u) / x in Nucl Q
let x, u be Element of Q; :: thesis: ( u in Nucl Q implies (x * u) / x in Nucl Q )
assume u in Nucl Q ; :: thesis: (x * u) / x in Nucl Q
then A1: ( u in Nucl_l Q & u in Nucl_m Q & u in Nucl_r Q ) by Th12;
deffunc H₁( Element of Q) -> Element of Q = (x * $1) / x;
consider t being Function of Q,Q such that
A2: for v being Element of Q holds t . v = H₁(v) from FUNCT_2:sch 4();
A3: t in InnAut Q

proof

reconsider g = (curry the multF of Q) . x, h = (curry' the multF of Q) . x as Permutation of Q by Th30, Th31;
A4: t = (h ") * g

proof

for u being Element of Q holds (h * t) . u = g . u

proof

let u be Element of Q; :: thesis: (h * t) . u = g . u
(h * t) . u = h . (t . u) by FUNCT_2:15
.= h . H₁(u) by A2
.= ((x * u) / x) * x by FUNCT_5:70
.= g . u by FUNCT_5:69 ;
hence (h * t) . u = g . u ; :: thesis: verum

end;

then (h ") * g = (h ") * (h * t) by FUNCT_2:def 8
.= ((h ") * h) * t by RELAT_1:36
.= (id the carrier of Q) * t by FUNCT_2:61
.= t by FUNCT_2:17 ;
hence t = (h ") * g ; :: thesis: verum

end;

A5: g in Mlt ([#] Q) by Th32;
h in Mlt ([#] Q) by Th33;
then A6: h " in Mlt ([#] Q) by Def35;
t . (1. Q) = (x * (1. Q)) / x by A2
.= 1. Q by Th6 ;
hence t in InnAut Q by Th55, A6, A4, Def34, A5; :: thesis: verum

end;

for y, z being Element of Q holds (H₁(u) * y) * z = H₁(u) * (y * z)

proof

let y, z be Element of Q; :: thesis: (H₁(u) * y) * z = H₁(u) * (y * z)
set f = R_MAP (y,z);
A8: R_MAP (y,z) in InnAut Q by Th58;
(R_MAP (y,z)) . u = R_map (u,y,z) by RM1
.= (u * (y * z)) / (y * z) by Def22, A1
.= u ;
then H₁(u) = t . ((R_MAP (y,z)) . u) by A2
.= (t * (R_MAP (y,z))) . u by FUNCT_2:15
.= ((R_MAP (y,z)) * t) . u by A8, Def50, A3
.= (R_MAP (y,z)) . (t . u) by FUNCT_2:15
.= (R_MAP (y,z)) . H₁(u) by A2
.= R_map (H₁(u),y,z) by RM1
.= ((H₁(u) * y) * z) / (y * z) ;
hence (H₁(u) * y) * z = H₁(u) * (y * z) ; :: thesis: verum

end;

then A9: H₁(u) in Nucl_l Q by Def22;
for y, z being Element of Q holds (y * z) * H₁(u) = y * (z * H₁(u))

proof

let y, z be Element of Q; :: thesis: (y * z) * H₁(u) = y * (z * H₁(u))
set f = L_MAP (z,y);
L_MAP (z,y) in InnAut Q by Th57;
then A11: t * (L_MAP (z,y)) = (L_MAP (z,y)) * t by Def50, A3;
(L_MAP (z,y)) . u = L_map (u,z,y) by LM1
.= (y * z) \ ((y * z) * u) by Def24, A1
.= u ;
then H₁(u) = t . ((L_MAP (z,y)) . u) by A2
.= (t * (L_MAP (z,y))) . u by FUNCT_2:15
.= (L_MAP (z,y)) . (t . u) by FUNCT_2:15, A11
.= (L_MAP (z,y)) . H₁(u) by A2
.= L_map (H₁(u),z,y) by LM1
.= (y * z) \ (y * (z * H₁(u))) ;
hence (y * z) * H₁(u) = y * (z * H₁(u)) ; :: thesis: verum

end;

then A12: H₁(u) in Nucl_r Q by Def24;
for y, z being Element of Q holds (y * H₁(u)) * z = y * (H₁(u) * z)

proof

let y, z be Element of Q; :: thesis: (y * H₁(u)) * z = y * (H₁(u) * z)
deffunc H₂( Element of Q) -> Element of Q = y \ ((y * ($1 * z)) / z);
A13: H₂(u) = y \ (((y * u) * z) / z) by Def23, A1
.= u ;
consider m being Function of Q,Q such that
A14: for v being Element of Q holds m . v = H₂(v) from FUNCT_2:sch 4();
A15: m in InnAut Q

proof

reconsider h = (curry' the multF of Q) . z, k = (curry the multF of Q) . y as Permutation of Q by Th31, Th30;
A16: ( h in Mlt ([#] Q) & k in Mlt ([#] Q) ) by Th32, Th33;
then A17: ( h " in Mlt ([#] Q) & k " in Mlt ([#] Q) ) by Def35;
k * h in Mlt ([#] Q) by A16, Def34;
then (h ") * (k * h) in Mlt ([#] Q) by A17, Def34;
then A18: (k ") * ((h ") * (k * h)) in Mlt ([#] Q) by A17, Def34;
A19: for v being Element of Q holds (h * k) . v = (y * v) * z

proof

let v be Element of Q; :: thesis: (h * k) . v = (y * v) * z
(h * k) . v = h . (k . v) by FUNCT_2:15
.= h . (y * v) by FUNCT_5:69
.= (y * v) * z by FUNCT_5:70 ;
hence (h * k) . v = (y * v) * z ; :: thesis: verum

end;

A20: for v being Element of Q holds (k * h) . v = y * (v * z)

proof

let v be Element of Q; :: thesis: (k * h) . v = y * (v * z)
(k * h) . v = k . (h . v) by FUNCT_2:15
.= k . (v * z) by FUNCT_5:70
.= y * (v * z) by FUNCT_5:69 ;
hence (k * h) . v = y * (v * z) ; :: thesis: verum

end;

for v being Element of Q holds m . v = ((k ") * ((h ") * (k * h))) . v

proof

let v be Element of Q; :: thesis: m . v = ((k ") * ((h ") * (k * h))) . v
(y * (m . v)) * z = (y * H₂(v)) * z by A14
.= (k * h) . v by A20
.= ((id the carrier of Q) * (k * h)) . v by FUNCT_2:17
.= ((h * (h ")) * (k * h)) . v by FUNCT_2:61
.= (h * ((h ") * (k * h))) . v by RELAT_1:36
.= (h * ((id the carrier of Q) * ((h ") * (k * h)))) . v by FUNCT_2:17
.= (h * ((k * (k ")) * ((h ") * (k * h)))) . v by FUNCT_2:61
.= (h * (k * ((k ") * ((h ") * (k * h))))) . v by RELAT_1:36
.= ((h * k) * ((k ") * ((h ") * (k * h)))) . v by RELAT_1:36
.= (h * k) . (((k ") * ((h ") * (k * h))) . v) by FUNCT_2:15
.= (y * (((k ") * ((h ") * (k * h))) . v)) * z by A19 ;
then y * (m . v) = y * (((k ") * ((h ") * (k * h))) . v) by Th2;
hence m . v = ((k ") * ((h ") * (k * h))) . v by Th1; :: thesis: verum

end;

then A21: m in Mlt ([#] Q) by A18, FUNCT_2:def 8;
m . (1. Q) = H₂( 1. Q) by A14
.= 1. Q by Th5 ;
hence m in InnAut Q by Def49, A21; :: thesis: verum

end;

A22: t * m = m * t by Def50, A15, A3;
H₂(H₁(u)) = m . H₁(u) by A14
.= m . (t . u) by A2
.= (t * m) . u by A22, FUNCT_2:15
.= t . (m . u) by FUNCT_2:15
.= t . H₂(u) by A14
.= H₁(u) by A13, A2 ;
hence (y * H₁(u)) * z = y * (H₁(u) * z) ; :: thesis: verum

end;

then H₁(u) in Nucl_m Q by Def23;
hence (x * u) / x in Nucl Q by Th12, A9, A12; :: thesis: verum