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
( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) )
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
( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) )
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 ( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) ) )
assume A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ; :: thesis: ( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) )
( Mlt H in bool (Funcs (Q,Q)) & phi is quasi_total ) ;
then A2: Mlt H in dom phi by FUNCT_2:def 1;
A3: phi . (Mlt H) c= Mlt H

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in phi . (Mlt H) or f in Mlt H )
assume f in phi . (Mlt H) ; :: thesis: f in Mlt H
then f in MltClos1 (H,(Mlt H)) by A1;
then S₂[Q,H, Mlt H,f] by Def37;
hence f in Mlt H by Th33, Th32, Def34, Def35; :: thesis: verum

end;

A4: for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S

proof

let S be Subset of (Funcs (Q,Q)); :: thesis: ( phi . S c= S implies Mlt H c= S )
assume A5: phi . S c= S ; :: thesis: Mlt H c= S
set SP = { f where f is Permutation of Q : f in S } ;
A6: { f where f is Permutation of Q : f in S } c= S

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { f where f is Permutation of Q : f in S } or g in S )
assume g in { f where f is Permutation of Q : f in S } ; :: thesis: g in S
then ex f being Permutation of Q st
( g = f & f in S ) ;
hence g in S ; :: thesis: verum

end;

S c= Funcs ( the carrier of Q, the carrier of Q) ;
then { f where f is Permutation of Q : f in S } c= Funcs ( the carrier of Q, the carrier of Q) by A6;
then reconsider SP = { f where f is Permutation of Q : f in S } as Subset of (Funcs ( the carrier of Q, the carrier of Q)) ;
A7: for f being Element of SP st f in SP holds
f is Permutation of the carrier of Q

proof

let f be Element of SP; :: thesis: ( f in SP implies f is Permutation of the carrier of Q )
assume f in SP ; :: thesis: f is Permutation of the carrier of Q
then ex g being Permutation of Q st
( f = g & g in S ) ;
hence f is Permutation of the carrier of Q ; :: thesis: verum

end;

for f, g being Element of SP st f in SP & g in SP holds
f * g in SP

proof

let f, g be Element of SP; :: thesis: ( f in SP & g in SP implies f * g in SP )
assume A8: ( f in SP & g in SP ) ; :: thesis: f * g in SP
reconsider f = f, g = g as Permutation of the carrier of Q by A7, A8;
f * g in MltClos1 (H,S) by Def37, A8, A6;
then f * g in phi . S by A1;
hence f * g in SP by A5; :: thesis: verum

end;

then A9: SP is composition-closed ;
for f being Element of SP st f in SP holds
f " in SP

proof

let f be Element of SP; :: thesis: ( f in SP implies f " in SP )
assume A10: f in SP ; :: thesis: f " in SP
then ( f in S & f is Permutation of Q ) by A6, A7;
then f " in MltClos1 (H,S) by Def37;
then A11: f " in phi . S by A1;
reconsider f = f as Permutation of Q by A10, A7;
f " is Permutation of Q ;
hence f " in SP by A11, A5; :: thesis: verum

end;

then SP is inverse-closed ;
then reconsider SP = SP as composition-closed inverse-closed Subset of (Funcs (Q,Q)) by A9;
for u being Element of Q st u in H holds
( (curry the multF of Q) . u in SP & (curry' the multF of Q) . u in SP )

proof

let u be Element of Q; :: thesis: ( u in H implies ( (curry the multF of Q) . u in SP & (curry' the multF of Q) . u in SP ) )
assume A12: u in H ; :: thesis: ( (curry the multF of Q) . u in SP & (curry' the multF of Q) . u in SP )
then (curry the multF of Q) . u in MltClos1 (H,S) by Def37;
then A13: (curry the multF of Q) . u in phi . S by A1;
(curry the multF of Q) . u is Permutation of Q by Th30;
hence (curry the multF of Q) . u in SP by A13, A5; :: thesis: (curry' the multF of Q) . u in SP
(curry' the multF of Q) . u in MltClos1 (H,S) by Def37, A12;
then A14: (curry' the multF of Q) . u in phi . S by A1;
(curry' the multF of Q) . u is Permutation of Q by Th31;
hence (curry' the multF of Q) . u in SP by A14, A5; :: thesis: verum

end;

then H left-right-mult-closed SP ;
then Mlt H c= SP by Def38;
hence Mlt H c= S by A6; :: thesis: verum

end;

Mlt H c= phi . (Mlt H)

proof

for f, g being Element of phi . (Mlt H) st f in phi . (Mlt H) & g in phi . (Mlt H) holds
f * g in phi . (Mlt H)

proof

let f, g be Element of phi . (Mlt H); :: thesis: ( f in phi . (Mlt H) & g in phi . (Mlt H) implies f * g in phi . (Mlt H) )
assume A15: ( f in phi . (Mlt H) & g in phi . (Mlt H) ) ; :: thesis: f * g in phi . (Mlt H)
then ( f is Permutation of Q & g is Permutation of Q ) by Th28, A1, A4, A3;
then f * g in MltClos1 (H,(Mlt H)) by Def37, A15, A3;
hence f * g in phi . (Mlt H) by A1; :: thesis: verum

end;

then A16: phi . (Mlt H) is composition-closed ;
for f being Element of phi . (Mlt H) st f in phi . (Mlt H) holds
f " in phi . (Mlt H)

proof

let f be Element of phi . (Mlt H); :: thesis: ( f in phi . (Mlt H) implies f " in phi . (Mlt H) )
assume A17: f in phi . (Mlt H) ; :: thesis: f " in phi . (Mlt H)
then f is Permutation of Q by A3, Th28, A1, A4;
then f " in MltClos1 (H,(Mlt H)) by Def37, A17, A3;
hence f " in phi . (Mlt H) by A1; :: thesis: verum

end;

then phi . (Mlt H) is inverse-closed ;
then reconsider S = phi . (Mlt H) as composition-closed inverse-closed Subset of (Funcs (Q,Q)) by A16;
for u being Element of Q st u in H holds
( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S )

proof

let u be Element of Q; :: thesis: ( u in H implies ( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S ) )
assume u in H ; :: thesis: ( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S )
then ( (curry the multF of Q) . u in MltClos1 (H,(Mlt H)) & (curry' the multF of Q) . u in MltClos1 (H,(Mlt H)) ) by Def37;
hence ( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S ) by A1; :: thesis: verum

end;

then H left-right-mult-closed S ;
hence Mlt H c= phi . (Mlt H) by Def38; :: thesis: verum

end;

then Mlt H = phi . (Mlt H) by A3;
hence ( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) ) by A4, ABIAN:def 3, A2; :: thesis: verum