reconsider Q1 = multLoopStr(# the carrier of Q, the multF of Q, the OneF of Q #) as non empty multLoopStr ;
the multF of Q1 = the multF of Q || the carrier of Q1 ;
then reconsider Q1 = Q1 as SubLoopStr of Q by Def30;
take Q1 ; :: thesis:

now :: thesis:

let x be Element of Q1; :: thesis:
reconsider x1 = x as Element of Q ;
( x * (1. Q1) = x1 * (1. Q) & (1. Q1) * x = (1. Q) * x1 ) ;
hence ( x * (1. Q1) = x & (1. Q1) * x = x ) ; :: thesis:

end;

hence Q1 is well-unital ; :: thesis:
thus Q1 is invertible :: thesis:

proof

hereby :: according to ALGSTR_1:def 6 :: thesis:

let x, y be Element of Q1; :: thesis:
reconsider x1 = x, y1 = y as Element of Q ;
reconsider z = x1 \ y1 as Element of Q1 ;
take z = z; :: thesis:
thus x * z = x1 * (x1 \ y1)
.= y ; :: thesis:

end;

hereby :: thesis:

let x, y be Element of Q1; :: thesis:
reconsider x1 = x, y1 = y as Element of Q ;
reconsider z = y1 / x1 as Element of Q1 ;
take z = z; :: thesis:
thus z * x = (y1 / x1) * x1
.= y ; :: thesis:

end;

end;

thus Q1 is cancelable :: thesis:

proof

thus Q1 is left_mult-cancelable :: according to ALGSTR_0:def 25 :: thesis:

proof

let x be Element of Q1; :: according to ALGSTR_0:def 23 :: thesis:
let y, z be Element of Q1; :: according to ALGSTR_0:def 20 :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
assume x * y = x * z ; :: thesis:
then x1 * y1 = x1 * z1 ;
hence y = z by ALGSTR_0:def 20; :: thesis:

end;

thus Q1 is right_mult-cancelable :: thesis:

proof

let x be Element of Q1; :: according to ALGSTR_0:def 24 :: thesis:
let y, z be Element of Q1; :: according to ALGSTR_0:def 21 :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
assume y * x = z * x ; :: thesis:
then y1 * x1 = z1 * x1 ;
hence y = z by ALGSTR_0:def 21; :: thesis:

end;

end;

thus ( not Q1 is empty & Q1 is strict ) ; :: thesis: