let Q be multLoop; :: thesis: for x, y being Element of Q holds L_MAP (x,y) in InnAut Q
let x, y be Element of Q; :: thesis: L_MAP (x,y) in InnAut Q
set f = L_MAP (x,y);
reconsider g = (curry the multF of Q) . (y * 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 Th30;
reconsider k = (curry the multF of Q) . y as Permutation of the carrier of Q by Th30;
A2: L_MAP (x,y) = (g ") * (k * h)

proof

for u being Element of Q holds (g * (L_MAP (x,y))) . u = (k * h) . u

proof

let u be Element of Q; :: thesis: (g * (L_MAP (x,y))) . u = (k * h) . u
(g * (L_MAP (x,y))) . u = g . ((L_MAP (x,y)) . u) by FUNCT_2:15
.= g . (L_map (u,x,y)) by LM1
.= (y * x) * ((y * x) \ (y * (x * u))) by FUNCT_5:69
.= k . (x * u) by FUNCT_5:69
.= k . (h . u) by FUNCT_5:69
.= (k * h) . u by FUNCT_2:15 ;
hence (g * (L_MAP (x,y))) . u = (k * h) . u ; :: thesis: verum

end;

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

end;

g in Mlt ([#] Q) by Th32;
then A3: g " in Mlt ([#] Q) by Def35;
( h in Mlt ([#] Q) & k in Mlt ([#] Q) ) by Th32;
then A4: k * h in Mlt ([#] Q) by Def34;
(L_MAP (x,y)) . (1. Q) = L_map ((1. Q),x,y) by LM1
.= 1. Q by Th5 ;
hence L_MAP (x,y) in InnAut Q by Th55, A4, A2, Def34, A3; :: thesis: verum