let Q be multLoop; :: thesis: 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 ) )
set H = Cent Q;
defpred S3[ 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
S3[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
S3[f]
proof
let u be Element of Q; :: thesis: ( u in Cent Q implies for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f] )
assume A3: u in Cent Q ; :: thesis: for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f]
then A4: u in Comm Q by XBOOLE_0:def 4;
let f be Function of Q,Q; :: thesis: ( ( for x being Element of Q holds f . x = u * x ) implies S3[f] )
assume A5: for x being Element of Q holds f . x = u * x ; :: thesis: S3[f]
S3[f]
proof
take u ; :: thesis: ( u in Cent Q & ( for x being Element of Q holds f . x = x * u ) )
thus u in Cent Q by A3; :: thesis: for x being Element of Q holds f . x = x * u
let x be Element of Q; :: thesis: f . x = x * u
f . x = u * x by A5
.= x * u by Def25, A4 ;
hence f . x = x * u ; :: thesis: verum
end;
hence S3[f] ; :: thesis: verum
end;
A6: for g, h being Permutation of Q st S3[g] & S3[h] holds
S3[g * h]
proof
let g, h be Permutation of Q; :: thesis: ( S3[g] & S3[h] implies S3[g * h] )
assume A7: ( S3[g] & S3[h] ) ; :: thesis: S3[g * h]
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: ( v * u in Cent Q & ( for x being Element of Q holds (g * h) . x = x * (v * u) ) )
( 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: for x being Element of Q holds (g * h) . x = x * (v * u)
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 = x * (v * u)
(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: verum
end;
A11: for g being Permutation of Q st S3[g] holds
S3[g " ]
proof
let g be Permutation of Q; :: thesis: ( S3[g] implies S3[g " ] )
assume S3[g] ; :: thesis: S3[g " ]
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;
S3[g " ]
proof
take v \ (1. Q) ; :: thesis: ( v \ (1. Q) in Cent Q & ( for x being Element of Q holds (g ") . x = x * (v \ (1. Q)) ) )
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: for x being Element of Q holds (g ") . x = x * (v \ (1. Q))
let x be Element of Q; :: thesis: (g ") . x = x * (v \ (1. Q))
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
proof
let y be Element of Q; :: thesis: (h * g) . y = (id Q) . y
(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: verum
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: verum
end;
hence S3[g " ] ; :: thesis: verum
end;
for f being Function of Q,Q st f in Mlt (Cent Q) holds
S3[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: verum