deffunc H1( Subset of Q) -> Subset of Q = loopclose1 (H,$1);
consider f being Function of (bool the carrier of Q),(bool the carrier of Q) such that
A1:
for X being Subset of Q holds f . X = H1(X)
from FUNCT_2:sch 4();
f is V278()
then reconsider f = f as V278() Function of (bool the carrier of Q),(bool the carrier of Q) ;
set LFP = lfp ( the carrier of Q,f);
lfp ( the carrier of Q,f) is_a_fixpoint_of f
by KNASTER:4;
then A3:
( lfp ( the carrier of Q,f) in dom f & lfp ( the carrier of Q,f) = f . (lfp ( the carrier of Q,f)) & f . (lfp ( the carrier of Q,f)) = H1( lfp ( the carrier of Q,f)) )
by ABIAN:def 3, A1;
A4:
1. Q in H1( lfp ( the carrier of Q,f))
by Def32;
reconsider ONE = 1. Q as Element of lfp ( the carrier of Q,f) by A3, Def32;
set mm = the multF of Q || (lfp ( the carrier of Q,f));
now for x being set st x in [:(lfp ( the carrier of Q,f)),(lfp ( the carrier of Q,f)):] holds
the multF of Q . x in lfp ( the carrier of Q,f)let x be
set ;
( x in [:(lfp ( the carrier of Q,f)),(lfp ( the carrier of Q,f)):] implies the multF of Q . x in lfp ( the carrier of Q,f) )assume A5:
x in [:(lfp ( the carrier of Q,f)),(lfp ( the carrier of Q,f)):]
;
the multF of Q . x in lfp ( the carrier of Q,f)consider x1,
x2 being
object such that A6:
(
x1 in lfp ( the
carrier of
Q,
f) &
x2 in lfp ( the
carrier of
Q,
f) &
x = [x1,x2] )
by A5, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
Q by A6;
x1 * x2 in H1(
lfp ( the
carrier of
Q,
f))
by A6, Def32;
hence
the
multF of
Q . x in lfp ( the
carrier of
Q,
f)
by A6, A3;
verum end;
then
lfp ( the carrier of Q,f) is Preserv of the multF of Q
by REALSET1:def 1;
then reconsider mm = the multF of Q || (lfp ( the carrier of Q,f)) as BinOp of (lfp ( the carrier of Q,f)) by REALSET1:2;
set LP = multLoopStr(# (lfp ( the carrier of Q,f)),mm,ONE #);
reconsider LP = multLoopStr(# (lfp ( the carrier of Q,f)),mm,ONE #) as non empty SubLoopStr of Q by A4, A3, Def30;
LP is SubLoop of Q
then reconsider LP = LP as strict SubLoop of Q ;
take
LP
; ( H c= [#] LP & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] LP c= [#] H2 ) )
thus
H c= [#] LP
by A3, Def32; for H2 being SubLoop of Q st H c= [#] H2 holds
[#] LP c= [#] H2
let H2 be SubLoop of Q; ( H c= [#] H2 implies [#] LP c= [#] H2 )
assume A9:
H c= [#] H2
; [#] LP c= [#] H2
reconsider H2c = [#] H2 as Subset of Q by Def30;
f . ([#] H2) c= [#] H2
then
f . H2c c= H2c
;
hence
[#] LP c= [#] H2
by KNASTER:6; verum