let Q be multLoop; :: thesis: for x being Element of Q holds T_MAP x in InnAut Q
let x be Element of Q; :: thesis: T_MAP x in InnAut Q
set f = T_MAP x;
reconsider g = (curry the multF of Q) . x as Permutation of the carrier of Q by Th30;
reconsider h = (curry' the multF of Q) . x as Permutation of the carrier of Q by Th31;
A2: T_MAP x = (g ") * h
proof
for u being Element of Q holds (g * (T_MAP x)) . u = h . u
proof
let u be Element of Q; :: thesis: (g * (T_MAP x)) . u = h . u
thus (g * (T_MAP x)) . u = g . ((T_MAP x) . u) by FUNCT_2:15
.= g . (T_map (u,x)) by TM1
.= x * (x \ (u * x)) by FUNCT_5:69
.= h . u by FUNCT_5:70 ; :: thesis: verum
end;
then (g ") * h = (g ") * (g * (T_MAP x)) by FUNCT_2:def 8
.= ((g ") * g) * (T_MAP x) by RELAT_1:36
.= (id the carrier of Q) * (T_MAP x) by FUNCT_2:61
.= T_MAP x by FUNCT_2:17 ;
hence T_MAP x = (g ") * h ; :: thesis: verum
end;
g in Mlt ([#] Q) by Th32;
then A3: g " in Mlt ([#] Q) by Def35;
A4: h in Mlt ([#] Q) by Th33;
(T_MAP x) . (1. Q) = T_map ((1. Q),x) by TM1
.= 1. Q by Th5 ;
hence T_MAP x in InnAut Q by A4, Th55, A2, Def34, A3; :: thesis: verum