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()
proof
let a1, b1 be set ; :: according to COHSP_1:def 11 :: thesis: ( not a1 in dom f or not b1 in dom f or not a1 c= b1 or f . a1 c= f . b1 )
assume A2: ( a1 in dom f & b1 in dom f & a1 c= b1 ) ; :: thesis: f . a1 c= f . b1
thus f . a1 c= f . b1 :: thesis: verum
proof
reconsider a2 = a1, b2 = b1 as Subset of Q by A2, FUNCT_2:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . a1 or x in f . b1 )
assume x in f . a1 ; :: thesis: x in f . b1
then x in H1(a2) by A1;
then ( x in H or x = 1. Q or S1[Q,a2,x] ) by Def32;
then x in H1(b2) by A2, Def32;
hence x in f . b1 by A1; :: thesis: verum
end;
end;
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 :: thesis: 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 ; :: thesis: ( 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)):] ; :: thesis: 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; :: thesis: 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
proof
now :: thesis: for x being Element of LP holds
( x * (1. LP) = x & (1. LP) * x = x )
let x be Element of LP; :: thesis: ( x * (1. LP) = x & (1. LP) * x = x )
x in the carrier of LP ;
then reconsider x1 = x as Element of Q ;
( x * (1. LP) = x1 * (1. Q) & (1. LP) * x = (1. Q) * x1 ) by RING_3:1;
hence ( x * (1. LP) = x & (1. LP) * x = x ) ; :: thesis: verum
end;
then A7: LP is well-unital ;
A8: LP is invertible
proof
hereby :: according to ALGSTR_1:def 6 :: thesis: for b1, b2 being Element of the carrier of LP ex b3 being Element of the carrier of LP st b3 * b1 = b2
let x, y be Element of LP; :: thesis: ex z being Element of LP st x * z = y
( x in the carrier of LP & y in the carrier of LP ) ;
then reconsider x1 = x, y1 = y as Element of Q ;
reconsider z = x1 \ y1 as Element of LP by Def32, A3;
take z = z; :: thesis: x * z = y
thus x * z = x1 * (x1 \ y1) by RING_3:1
.= y ; :: thesis: verum
end;
hereby :: thesis: verum
let x, y be Element of LP; :: thesis: ex z being Element of LP st z * x = y
( x in the carrier of LP & y in the carrier of LP ) ;
then reconsider x1 = x, y1 = y as Element of Q ;
reconsider z = y1 / x1 as Element of LP by Def32, A3;
take z = z; :: thesis: z * x = y
thus z * x = (y1 / x1) * x1 by RING_3:1
.= y ; :: thesis: verum
end;
end;
LP is cancelable
proof
thus LP is left_mult-cancelable :: according to ALGSTR_0:def 25 :: thesis: LP is right_mult-cancelable
proof
let x be Element of LP; :: according to ALGSTR_0:def 23 :: thesis: x is left_mult-cancelable
let y, z be Element of LP; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )
( x in the carrier of LP & y in the carrier of LP & z in the carrier of LP ) ;
then reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
( x1 * y1 = x * y & x1 * z1 = x * z ) by RING_3:1;
hence ( not x * y = x * z or y = z ) by ALGSTR_0:def 20; :: thesis: verum
end;
let x be Element of LP; :: according to ALGSTR_0:def 24 :: thesis: x is right_mult-cancelable
let y, z be Element of LP; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )
( x in the carrier of LP & y in the carrier of LP & z in the carrier of LP ) ;
then reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
( y1 * x1 = y * x & z1 * x1 = z * x ) by RING_3:1;
hence ( not y * x = z * x or y = z ) by ALGSTR_0:def 21; :: thesis: verum
end;
hence LP is SubLoop of Q by A7, A8; :: thesis: verum
end;
then reconsider LP = LP as strict SubLoop of Q ;
take LP ; :: thesis: ( H c= [#] LP & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] LP c= [#] H2 ) )
thus H c= [#] LP by A3, Def32; :: thesis: for H2 being SubLoop of Q st H c= [#] H2 holds
[#] LP c= [#] H2
let H2 be SubLoop of Q; :: thesis: ( H c= [#] H2 implies [#] LP c= [#] H2 )
assume A9: H c= [#] H2 ; :: thesis: [#] LP c= [#] H2
reconsider H2c = [#] H2 as Subset of Q by Def30;
f . ([#] H2) c= [#] H2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . ([#] H2) or x in [#] H2 )
assume x in f . ([#] H2) ; :: thesis: x in [#] H2
then A10: x in H1(H2c) by A1;
then reconsider xx = x as Element of Q ;
per cases ( x in H or x = 1. Q or S1[Q,H2c,x] ) by A10, Def32;
suppose x in H ; :: thesis: x in [#] H2
hence x in [#] H2 by A9; :: thesis: verum
end;
suppose S1[Q,H2c,x] ; :: thesis: x in [#] H2
then consider y, z being Element of Q such that
A11: ( y in H2c & z in H2c & ( x = y * z or x = y \ z or x = y / z ) ) ;
reconsider y1 = y, z1 = z as Element of H2 by A11;
( y1 \ z1 in H2c & y1 / z1 in H2c ) ;
then reconsider yz = y1 \ z1, YZ = y1 / z1 as Element of Q ;
the multF of H2 = the multF of Q || H2c by Def30;
then ( y * z = y1 * z1 & y * yz = y1 * (y1 \ z1) & y1 * (y1 \ z1) = z & YZ * z = (y1 / z1) * z1 & (y1 / z1) * z1 = y ) by RING_3:1;
hence x in [#] H2 by A11; :: thesis: verum
end;
end;
end;
then f . H2c c= H2c ;
hence [#] LP c= [#] H2 by KNASTER:6; :: thesis: verum