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: ( Q1 is well-unital & Q1 is invertible & Q1 is cancelable & not Q1 is empty & Q1 is strict )

now :: thesis: for x being Element of Q1 holds
( x * (1. Q1) = x & (1. Q1) * x = x )

let x be Element of Q1; :: thesis: ( x * (1. Q1) = x & (1. Q1) * x = x )
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: verum

end;

hence Q1 is well-unital ; :: thesis: ( Q1 is invertible & Q1 is cancelable & not Q1 is empty & Q1 is strict )
thus Q1 is invertible :: thesis: ( Q1 is cancelable & not Q1 is empty & Q1 is strict )

proof

hereby :: according to ALGSTR_1:def 6 :: thesis: for b₁, b₂ being Element of the carrier of Q1 ex b₃ being Element of the carrier of Q1 st b₃ * b₁ = b₂

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

end;

hereby :: thesis: verum

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

end;

end;

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

proof

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

proof

let x be Element of Q1; :: according to ALGSTR_0:def 23 :: thesis: x is left_mult-cancelable
let y, z be Element of Q1; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )
reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
assume x * y = x * z ; :: thesis: y = z
then x1 * y1 = x1 * z1 ;
hence y = z by ALGSTR_0:def 20; :: thesis: verum

end;

thus Q1 is right_mult-cancelable :: thesis: verum

proof

let x be Element of Q1; :: according to ALGSTR_0:def 24 :: thesis: x is right_mult-cancelable
let y, z be Element of Q1; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )
reconsider x1 = x, y1 = y, z1 = z as Element of Q ;
assume y * x = z * x ; :: thesis: y = z
then y1 * x1 = z1 * x1 ;
hence y = z by ALGSTR_0:def 21; :: thesis: verum

end;

end;

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