let Q be multLoop; :: thesis:
set H = Cent Q;
defpred S₃[ Function of Q,Q] means ex z being Element of Q st
( z in Cent Q & ( for x being Element of Q holds $1 . x = x * z ) );
A1: for u being Element of Q st u in Cent Q holds
for f being Function of Q,Q st ( for x being Element of Q holds f . x = x * u ) holds
S₃[f] ;
A2: for u being Element of Q st u in Cent Q holds
for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S₃[f]

take u ; :: thesis:
thus u in Cent Q by A3; :: thesis:
let x be Element of Q; :: thesis:
f . x = u * x by A5
.= x * u by Def25, A4 ;
hence f . x = x * u ; :: thesis:

end;

end;

A6: for g, h being Permutation of Q st S₃[g] & S₃[h] holds
S₃[g * h]

let g, h be Permutation of Q; :: thesis:
assume A7: ( S₃[g] & S₃[h] ) ; :: thesis:
consider u being Element of Q such that
A8: ( u in Cent Q & ( for x being Element of Q holds g . x = x * u ) ) by A7;
consider v being Element of Q such that
A9: ( v in Cent Q & ( for x being Element of Q holds h . x = x * v ) ) by A7;
take v * u ; :: thesis:
( u in [#] (lp (Cent Q)) & v in [#] (lp (Cent Q)) ) by Th25, A8, A9;
then v * u in [#] (lp (Cent Q)) by Th37;
hence v * u in Cent Q by Th25; :: thesis:
u in Nucl Q by A8, XBOOLE_0:def 4;
then A10: u in Nucl_r Q by Th12;
let x be Element of Q; :: thesis:
(g * h) . x = g . (h . x) by FUNCT_2:15
.= g . (x * v) by A9
.= (x * v) * u by A8
.= x * (v * u) by A10, Def24 ;
hence (g * h) . x = x * (v * u) ; :: thesis:

end;

A11: for g being Permutation of Q st S₃[g] holds
S₃[g " ]

let g be Permutation of Q; :: thesis:
assume S₃[g] ; :: thesis:
then consider v being Element of Q such that
A12: ( v in Cent Q & ( for x being Element of Q holds g . x = x * v ) ) ;
v in Nucl Q by A12, XBOOLE_0:def 4;
then A13: v in Nucl_m Q by Th12;
S₃[g " ]

take v \ (1. Q) ; :: thesis:
A14: 1. Q in [#] (lp (Cent Q)) by Th50;
v in [#] (lp (Cent Q)) by Th25, A12;
then v \ (1. Q) in [#] (lp (Cent Q)) by Th39, A14;
hence v \ (1. Q) in Cent Q by Th25; :: thesis:
let x be Element of Q; :: thesis:
reconsider h = (curry' the multF of Q) . (v \ (1. Q)) as Permutation of Q by Th31;
for y being Element of Q holds (h * g) . y = (id Q) . y

let y be Element of Q; :: thesis:
(h * g) . y = h . (g . y) by FUNCT_2:15
.= h . (y * v) by A12
.= (y * v) * (v \ (1. Q)) by FUNCT_5:70
.= y * (v * (v \ (1. Q))) by Def23, A13
.= y ;
hence (h * g) . y = (id Q) . y ; :: thesis:

end;

then (g ") . x = h . x by FUNCT_2:60, FUNCT_2:def 8
.= x * (v \ (1. Q)) by FUNCT_5:70 ;
hence (g ") . x = x * (v \ (1. Q)) ; :: thesis:

end;

end;

for f being Function of Q,Q st f in Mlt (Cent Q) holds
S₃[f] from AIMLOOP:sch 1(A1, A2, A6, A11);
hence for f being Function of Q,Q st f in Mlt (Cent Q) holds
ex z being Element of Q st
( z in Cent Q & ( for x being Element of Q holds f . x = x * z ) ) ; :: thesis: