let Q be multLoop; :: thesis: for x, y being Element of Q holds R_MAP (x,y) in InnAut Q
let x, y be Element of Q; :: thesis: R_MAP (x,y) in InnAut Q
set f = R_MAP (x,y);
reconsider g = (curry' the multF of Q) . (x * y) as Permutation of the carrier of Q by Th31;
reconsider h = (curry' the multF of Q) . x as Permutation of the carrier of Q by Th31;
reconsider k = (curry' the multF of Q) . y as Permutation of the carrier of Q by Th31;
A2: R_MAP (x,y) = (g ") * (k * h)

proof

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

proof

let u be Element of Q; :: thesis: (g * (R_MAP (x,y))) . u = (k * h) . u
thus (g * (R_MAP (x,y))) . u = g . ((R_MAP (x,y)) . u) by FUNCT_2:15
.= g . (R_map (u,x,y)) by RM1
.= (((u * x) * y) / (x * y)) * (x * y) by FUNCT_5:70
.= k . (u * x) by FUNCT_5:70
.= k . (h . u) by FUNCT_5:70
.= (k * h) . u by FUNCT_2:15 ; :: thesis: verum

end;

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

end;

g in Mlt ([#] Q) by Th33;
then A3: g " in Mlt ([#] Q) by Def35;
( h in Mlt ([#] Q) & k in Mlt ([#] Q) ) by Th33;
then A4: k * h in Mlt ([#] Q) by Def34;
(R_MAP (x,y)) . (1. Q) = R_map ((1. Q),x,y) by RM1
.= 1. Q by Th6 ;
hence R_MAP (x,y) in InnAut Q by Th55, A4, A2, Def34, A3; :: thesis: verum