let Q be multLoop; :: thesis: for H being Subset of Q st 1. Q in H & ( for x, y being Element of Q st x in H & y in H holds
x * y in H ) & ( for x, y being Element of Q st x in H & y in H holds
x \ y in H ) & ( for x, y being Element of Q st x in H & y in H holds
x / y in H ) holds
[#] (lp H) = H
let H be Subset of Q; :: thesis: ( 1. Q in H & ( for x, y being Element of Q st x in H & y in H holds
x * y in H ) & ( for x, y being Element of Q st x in H & y in H holds
x \ y in H ) & ( for x, y being Element of Q st x in H & y in H holds
x / y in H ) implies [#] (lp H) = H )
assume that
A1: 1. Q in H and
A2: for x, y being Element of Q st x in H & y in H holds
x * y in H and
A3: for x, y being Element of Q st x in H & y in H holds
x \ y in H and
A4: for x, y being Element of Q st x in H & y in H holds
x / y in H ; :: thesis: [#] (lp H) = H
reconsider ONE = 1. Q as Element of H by A1;
set mm = the multF of Q || H;

now :: thesis: for x being set st x in [:H,H:] holds
the multF of Q . x in H

let x be set ; :: thesis: ( x in [:H,H:] implies the multF of Q . x in H )
assume A5: x in [:H,H:] ; :: thesis: the multF of Q . x in H
consider x1, x2 being object such that
A6: ( x1 in H & x2 in H & x = [x1,x2] ) by A5, ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of Q by A6;
x1 * x2 in H by A6, A2;
hence the multF of Q . x in H by A6; :: thesis: verum

end;

then H is Preserv of the multF of Q by REALSET1:def 1;
then reconsider mm = the multF of Q || H as BinOp of H by REALSET1:2;
set LP = multLoopStr(# H,mm,ONE #);
reconsider LP = multLoopStr(# H,mm,ONE #) as non empty SubLoopStr of Q by A1, 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 b₁, b₂ being Element of the carrier of LP ex b₃ being Element of the carrier of LP st b₃ * b₁ = b₂

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 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 A4;
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 ;
( [#] (lp H) c= [#] LP & [#] LP = H ) by Def33;
hence [#] (lp H) = H by Def33; :: thesis: verum