let Q be multLoop; :: thesis:
let N be normal SubLoop of Q; :: thesis:
A1: the carrier of N c= the carrier of Q by Def30;
set f = QuotientHom (Q,N);
for x being Element of Q holds
( x in Ker (QuotientHom (Q,N)) iff x in @ ([#] N) )

let x be Element of Q; :: thesis:
thus ( x in Ker (QuotientHom (Q,N)) implies x in @ ([#] N) ) :: thesis:

assume A2: x in Ker (QuotientHom (Q,N)) ; :: thesis:
A3: x * N = (QuotientHom (Q,N)) . x by Def48
.= 1. (Q _/_ N) by Def29, A2
.= (1. Q) * N ;
A4: 1. N = 1. Q by Def30;
reconsider h = (curry the multF of Q) . (1. Q) as Permutation of Q by Th30;
A5: h in Mlt (@ ([#] N)) by A4, Th32;
A6: h . x in x * (@ ([#] N)) by Def39, A5;
h . x = (1. Q) * x by FUNCT_5:69;
hence x in @ ([#] N) by A6, A3, Th43; :: thesis:

end;

assume A7: x in @ ([#] N) ; :: thesis:
A8: for y being Element of Q holds
( y in x * N iff y in (1. Q) * N )

let y be Element of Q; :: thesis:
thus ( y in x * N implies y in (1. Q) * N ) :: thesis:

assume y in x * N ; :: thesis:
then consider h being Permutation of Q such that
A9: ( h in Mlt (@ ([#] N)) & h . x = y ) by Def39;
h . x in @ ([#] N) by Th42, A9, A7;
hence y in (1. Q) * N by A9, Th43; :: thesis:

end;

assume y in (1. Q) * N ; :: thesis:
then reconsider y1 = y as Element of N by Th43;
reconsider x1 = x as Element of N by A7;
ex h being Permutation of Q st
( h in Mlt (@ ([#] N)) & y = h . x )

reconsider y1x1 = y1 / x1 as Element of Q by A1;
reconsider h = (curry the multF of Q) . y1x1 as Permutation of Q by Th30;
take h ; :: thesis:
thus h in Mlt (@ ([#] N)) by Th32; :: thesis:
h . x = y1x1 * x by FUNCT_5:69
.= (y / x) * x by Th40
.= y ;
hence h . x = y ; :: thesis:

end;

end;

(QuotientHom (Q,N)) . x = x * N by Def48
.= 1. (Q _/_ N) by A8, SUBSET_1:3 ;
hence x in Ker (QuotientHom (Q,N)) by Def29; :: thesis:

end;