let Q be multLoop; :: thesis: for H being Subset of Q
for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds
for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q
let H be Subset of Q; :: thesis: for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds
for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q
let phi be Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))); :: thesis: ( ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) implies for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q )
assume A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ; :: thesis: for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q
let Y be Subset of (Funcs (Q,Q)); :: thesis: ( ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) implies for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q )
assume A2: for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ; :: thesis: for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q
set SP = { f where f is Permutation of Q : verum } ;
{ f where f is Permutation of Q : verum } c= Funcs (Q,Q)
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { f where f is Permutation of Q : verum } or f in Funcs (Q,Q) )
assume f in { f where f is Permutation of Q : verum } ; :: thesis: f in Funcs (Q,Q)
then consider g being Permutation of Q such that
A3: f = g ;
thus f in Funcs (Q,Q) by FUNCT_2:9, A3; :: thesis: verum
end;
then reconsider SP = { f where f is Permutation of Q : verum } as Subset of (Funcs (Q,Q)) ;
phi . SP c= SP
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in phi . SP or f in SP )
assume f in phi . SP ; :: thesis: f in SP
then f in MltClos1 (H,SP) by A1;
per cases then ( ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of the carrier of Q st
( g in SP & h in SP & f = g * h ) or ex g being Permutation of the carrier of Q st
( g in SP & f = g " ) ) by Def37;
suppose ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) ; :: thesis: f in SP
then consider u being Element of Q such that
A4: ( u in H & f = (curry' the multF of Q) . u ) ;
reconsider f = f as Function of Q,Q by A4;
deffunc H1( Element of Q) -> Element of Q = $1 / u;
consider g being Function of Q,Q such that
A5: for x being Element of Q holds g . x = H1(x) from FUNCT_2:sch 4();
 for x being Element of Q holds (g * f) . x = (id the carrier of Q) . x
proof
let x be Element of Q; :: thesis: (g * f) . x = (id the carrier of Q) . x
(g * f) . x = g . (f . x) by FUNCT_2:15
.= g . (x * u) by FUNCT_5:70, A4
.= H1(x * u) by A5
.= (id the carrier of Q) . x ;
hence (g * f) . x = (id the carrier of Q) . x ; :: thesis: verum
end;
then A6: g * f = id the carrier of Q by FUNCT_2:def 8;
for x being Element of Q holds (f * g) . x = (id the carrier of Q) . x
proof
let x be Element of Q; :: thesis: (f * g) . x = (id the carrier of Q) . x
(f * g) . x = f . (g . x) by FUNCT_2:15
.= (g . x) * u by FUNCT_5:70, A4
.= H1(x) * u by A5
.= (id the carrier of Q) . x ;
hence (f * g) . x = (id the carrier of Q) . x ; :: thesis: verum
end;
then rng f = the carrier of Q by FUNCT_2:18, FUNCT_2:def 8;
then f is Permutation of the carrier of Q by FUNCT_2:57, A6, FUNCT_2:31;
hence f in SP ; :: thesis: verum
end;
suppose ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) ; :: thesis: f in SP
then consider u being Element of Q such that
A7: ( u in H & f = (curry the multF of Q) . u ) ;
reconsider f = f as Function of Q,Q by A7;
deffunc H1( Element of Q) -> Element of Q = u \ $1;
consider g being Function of Q,Q such that
A8: for x being Element of Q holds g . x = H1(x) from FUNCT_2:sch 4();
A9: for x being Element of Q holds (g * f) . x = (id the carrier of Q) . x
proof
let x be Element of Q; :: thesis: (g * f) . x = (id the carrier of Q) . x
(g * f) . x = g . (f . x) by FUNCT_2:15
.= g . (u * x) by FUNCT_5:69, A7
.= H1(u * x) by A8
.= (id the carrier of Q) . x ;
hence (g * f) . x = (id the carrier of Q) . x ; :: thesis: verum
end;
A10: for x being Element of Q holds (f * g) . x = (id the carrier of Q) . x
proof
let x be Element of Q; :: thesis: (f * g) . x = (id the carrier of Q) . x
(f * g) . x = f . (g . x) by FUNCT_2:15
.= u * (g . x) by FUNCT_5:69, A7
.= u * H1(x) by A8
.= (id the carrier of Q) . x ;
hence (f * g) . x = (id the carrier of Q) . x ; :: thesis: verum
end;
A11: f is one-to-one by A9, FUNCT_2:31, FUNCT_2:def 8;
rng f = the carrier of Q by A10, FUNCT_2:18, FUNCT_2:def 8;
then f is Permutation of the carrier of Q by FUNCT_2:57, A11;
hence f in SP ; :: thesis: verum
end;
suppose ex g, h being Permutation of the carrier of Q st
( g in SP & h in SP & f = g * h ) ; :: thesis: f in SP
hence f in SP ; :: thesis: verum
end;
suppose ex g being Permutation of the carrier of Q st
( g in SP & f = g " ) ; :: thesis: f in SP
hence f in SP ; :: thesis: verum
end;
end;
end;
then A12: Y c= SP by A2;
let f be Element of Funcs (Q,Q); :: thesis: ( f in Y implies f is Permutation of Q )
assume f in Y ; :: thesis: f is Permutation of Q
then f in SP by A12;
then ex g being Permutation of Q st f = g ;
hence f is Permutation of Q ; :: thesis: verum