let Q be AIM multLoop; :: thesis: for x, u being Element of Q st u in Nucl Q holds
T_map (u,x) in Nucl Q
let x, u be Element of Q; :: thesis: ( u in Nucl Q implies T_map (u,x) in Nucl Q )
assume u in Nucl Q ; :: thesis: T_map (u,x) in Nucl Q
then A1: ( u in Nucl_l Q & u in Nucl_m Q & u in Nucl_r Q ) by Th12;
for y, z being Element of Q holds ((T_map (u,x)) * y) * z = (T_map (u,x)) * (y * z)
proof
let y, z be Element of Q; :: thesis: ((T_map (u,x)) * y) * z = (T_map (u,x)) * (y * z)
Q is satisfying_TR ;
then R_map ((T_map (u,x)),y,z) = T_map ((R_map (u,y,z)),x)
.= T_map (((u * (y * z)) / (y * z)),x) by Def22, A1
.= T_map (u,x) ;
hence ((T_map (u,x)) * y) * z = (T_map (u,x)) * (y * z) ; :: thesis: verum
end;
then A2: T_map (u,x) in Nucl_l Q by Def22;
for y, z being Element of Q holds (y * z) * (T_map (u,x)) = y * (z * (T_map (u,x)))
proof
let y, z be Element of Q; :: thesis: (y * z) * (T_map (u,x)) = y * (z * (T_map (u,x)))
Q is satisfying_TL ;
then L_map ((T_map (u,x)),z,y) = T_map ((L_map (u,z,y)),x)
.= T_map (((y * z) \ ((y * z) * u)),x) by Def24, A1
.= T_map (u,x) ;
hence (y * z) * (T_map (u,x)) = y * (z * (T_map (u,x))) ; :: thesis: verum
end;
then A3: T_map (u,x) in Nucl_r Q by Def24;
for y, z being Element of Q holds (y * (T_map (u,x))) * z = y * ((T_map (u,x)) * z)
proof
let y, z be Element of Q; :: thesis: (y * (T_map (u,x))) * z = y * ((T_map (u,x)) * z)
deffunc H1( Element of Q) -> Element of Q = y \ ((y * ($1 * z)) / z);
A4: H1(u) = y \ (((y * u) * z) / z) by Def23, A1
.= u ;
consider m being Function of Q,Q such that
A5: for v being Element of Q holds m . v = H1(v) from FUNCT_2:sch 4();
 A6: 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;
A7: ( h in Mlt ([#] Q) & k in Mlt ([#] Q) ) by Th32, Th33;
then A8: ( h " in Mlt ([#] Q) & k " in Mlt ([#] Q) ) by Def35;
k * h in Mlt ([#] Q) by A7, Def34;
then (h ") * (k * h) in Mlt ([#] Q) by A8, Def34;
then A9: (k ") * ((h ") * (k * h)) in Mlt ([#] Q) by A8, Def34;
A10: 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;
A11: 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 * H1(v)) * z by A5
.= (k * h) . v by A11
.= ((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 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 A10 ;
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 A12: m in Mlt ([#] Q) by A9, FUNCT_2:def 8;
m . (1. Q) = H1( 1. Q) by A5
.= 1. Q by Th5 ;
hence m in InnAut Q by Def49, A12; :: thesis: verum
end;
set t = T_MAP x;
T_MAP x in InnAut Q by Th56;
then A14: (T_MAP x) * m = m * (T_MAP x) by Def50, A6;
H1( T_map (u,x)) = m . (T_map (u,x)) by A5
.= m . ((T_MAP x) . u) by TM1
.= (m * (T_MAP x)) . u by FUNCT_2:15
.= (T_MAP x) . (m . u) by FUNCT_2:15, A14
.= (T_MAP x) . H1(u) by A5
.= T_map (u,x) by A4, TM1 ;
hence (y * (T_map (u,x))) * z = y * ((T_map (u,x)) * z) ; :: thesis: verum
end;
then T_map (u,x) in Nucl_m Q by Def23;
hence T_map (u,x) in Nucl Q by Th12, A2, A3; :: thesis: verum