end;

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

let S be Subset of (Funcs (Q,Q)); :: thesis:
assume A5: phi . S c= S ; :: thesis:
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

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

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

end;

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

let f, g be Element of SP; :: thesis:
assume A8: ( f in SP & g in SP ) ; :: thesis:
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:

end;

let f be Element of SP; :: thesis:
assume A10: f in SP ; :: thesis:
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:

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 )

let u be Element of Q; :: thesis:
assume A12: u in H ; :: thesis:
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 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:

end;

end;

Mlt H c= phi . (Mlt H)

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)

let f, g be Element of phi . (Mlt H); :: thesis:
assume A15: ( f in phi . (Mlt H) & g in phi . (Mlt H) ) ; :: thesis:
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:

end;

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 )

let u be Element of Q; :: thesis:
assume u in H ; :: thesis:
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:

end;

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: