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 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; :: 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 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))); :: 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 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) ; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( Y is composition-closed & Y is inverse-closed )
thus Y is composition-closed :: thesis: Y is inverse-closed
proof
let f, g be Element of Y; :: according to AIMLOOP:def 36 :: thesis: ( f in Y & g in Y implies f * g in Y )
assume A4: ( f in Y & g in Y ) ; :: thesis: f * g in Y
then ( f is Permutation of Q & g is Permutation of Q ) by Th28, A1, A3;
hence f * g in Y by A2, Def37, A4; :: thesis: verum
end;
let f be Element of Y; :: according to AIMLOOP:def 37 :: thesis: ( f in Y implies f " in Y )
assume A5: f in Y ; :: thesis: f " in Y
then f is Permutation of Q by Th28, A1, A3;
hence f " in Y by A2, Def37, A5; :: thesis: verum