let Q be multLoop; :: thesis: for N being normal SubLoop of Q holds the carrier of N = (1. Q) * N
let N be normal SubLoop of Q; :: thesis: the carrier of N = (1. Q) * N
A1: the carrier of N c= the carrier of Q by Def30;
thus the carrier of N c= (1. Q) * N :: according to XBOOLE_0:def 10 :: thesis: (1. Q) * N c= the carrier of N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of N or x in (1. Q) * N )
assume A2: x in the carrier of N ; :: thesis: x in (1. Q) * N
then reconsider x = x as Element of Q by A1;
A3: (curry the multF of Q) . x in Mlt (@ ([#] N)) by Th32, A2;
reconsider h = (curry the multF of Q) . x as Permutation of Q by Th30;
h . (1. Q) = x * (1. Q) by FUNCT_5:69;
hence x in (1. Q) * N by Def39, A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (1. Q) * N or x in the carrier of N )
assume x in (1. Q) * N ; :: thesis: x in the carrier of N
then A4: ex h being Permutation of Q st
( h in Mlt (@ ([#] N)) & x = h . (1. Q) ) by Def39;
1. N = 1. Q by Def30;
hence x in the carrier of N by Th42, A4; :: thesis: verum