let Q be multLoop; :: thesis:
let H be Subset of Q; :: thesis:
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:
reconsider ONE = 1. Q as Element of H by A1;
set mm = the multF of Q || H;

let x be set ; :: thesis:
assume A5: x in [:H,H:] ; :: thesis:
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:

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

let x be Element of LP; :: thesis:
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:

end;

let x, y be Element of LP; :: thesis:
( 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:
thus x * z = x1 * (x1 \ y1) by RING_3:1
.= y ; :: thesis:

end;

let x, y be Element of LP; :: thesis:
( 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:
thus z * x = (y1 / x1) * x1 by RING_3:1
.= y ; :: thesis:

end;

let x be Element of LP; :: according to ALGSTR_0:def 23 :: thesis:
let y, z be Element of LP; :: according to ALGSTR_0:def 20 :: thesis:
( 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:

end;

let x be Element of LP; :: according to ALGSTR_0:def 24 :: thesis:
let y, z be Element of LP; :: according to ALGSTR_0:def 21 :: thesis:
( 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:

end;

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: