reconsider Q1 = Q as non empty multLoopStr ;
A1: the multF of Q1 = the multF of Q || the carrier of Q1 ;
the OneF of Q1 = the OneF of Q ;
then reconsider Q1 = Q1 as SubLoop of Q by A1, Def30;
take Q1 ; :: thesis:
A2: for x, y being Element of Q holds y in x * Q1

proof

let x, y be Element of Q; :: thesis:
ex g being Permutation of Q st
( g in Mlt (@ ([#] Q1)) & y = g . x )

proof

reconsider g = (curry the multF of Q) . (y / x) as Permutation of Q by Th30;
A3: @ ([#] Q1) left-right-mult-closed Mlt (@ ([#] Q1)) by Def38;
g . x = (y / x) * x by FUNCT_5:69
.= y ;
hence ex g being Permutation of Q st
( g in Mlt (@ ([#] Q1)) & y = g . x ) by A3; :: thesis:

end;

hence y in x * Q1 by Def39; :: thesis:

end;

A5: for x, y being Element of Q holds x * Q1 = y * Q1

proof

let x, y be Element of Q; :: thesis:
for v being Element of Q holds
( v in x * Q1 iff v in y * Q1 ) by A2;
hence x * Q1 = y * Q1 by SUBSET_1:3; :: thesis:

end;

now :: thesis:

let x, y be Element of Q; :: thesis:
for v being Element of Q holds
( v in (x * Q1) * (y * Q1) iff v in (x * y) * Q1 )

proof

let v be Element of Q; :: thesis:
thus ( v in (x * Q1) * (y * Q1) implies v in (x * y) * Q1 ) by A2; :: thesis:
assume v in (x * y) * Q1 ; :: thesis:
ex u, w being Element of Q st
( u in x * Q1 & w in y * Q1 & v = u * w )

proof

take v ; :: thesis:
take 1. Q ; :: thesis:
thus ( v in x * Q1 & 1. Q in y * Q1 & v = v * (1. Q) ) by A2; :: thesis:

end;

hence v in (x * Q1) * (y * Q1) by Def42; :: thesis:

end;

hence (x * Q1) * (y * Q1) = (x * y) * Q1 by SUBSET_1:3; :: thesis:
let z be Element of Q; :: thesis:
thus ( (x * Q1) * (z * Q1) = (y * Q1) * (z * Q1) implies x * Q1 = y * Q1 ) by A5; :: thesis:
thus ( (z * Q1) * (x * Q1) = (z * Q1) * (y * Q1) implies x * Q1 = y * Q1 ) by A5; :: thesis:

end;

hence Q1 is normal ; :: thesis: