let Q be multLoop; :: thesis: for H being Subset of Q
for f being Element of Funcs (Q,Q) st f in Mlt H holds
f is Permutation of Q
let H be Subset of Q; :: thesis: for f being Element of Funcs (Q,Q) st f in Mlt H holds
f is Permutation of Q
deffunc H₁( Subset of (Funcs (Q,Q))) -> Subset of (Funcs (Q,Q)) = MltClos1 (H,$1);
consider phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) such that
A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = H₁(X) from FUNCT_2:sch 4();
for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S by Th34, A1;
hence for f being Element of Funcs (Q,Q) st f in Mlt H holds
f is Permutation of Q by Th28, A1; :: thesis: verum