let Q be multLoop; 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 Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
( Y is composition-closed & Y is inverse-closed )
let H be 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 Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
( Y is composition-closed & Y is inverse-closed )
let phi be Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))); ( ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) implies for Y being Subset of (Funcs (Q,Q)) st Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
( Y is composition-closed & Y is inverse-closed ) )
assume A1:
for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X)
; for Y being Subset of (Funcs (Q,Q)) st Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
( Y is composition-closed & Y is inverse-closed )
let Y be Subset of (Funcs (Q,Q)); ( Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) implies ( Y is composition-closed & Y is inverse-closed ) )
assume
Y is_a_fixpoint_of phi
; ( ex S being Subset of (Funcs (Q,Q)) st
( phi . S c= S & not Y c= S ) or ( Y is composition-closed & Y is inverse-closed ) )
then A2:
( Y in dom phi & Y = phi . Y & phi . Y = MltClos1 (H,Y) )
by ABIAN:def 3, A1;
assume A3:
for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S
; ( Y is composition-closed & Y is inverse-closed )
thus
Y is composition-closed
Y is inverse-closed
let f be Element of Y; AIMLOOP:def 37 ( f in Y implies f " in Y )
assume A5:
f in Y
; f " in Y
then
f is Permutation of Q
by Th28, A1, A3;
hence
f " in Y
by A2, Def37, A5; verum