let Q be multLoop; :: thesis: for N being normal SubLoop of Q holds Ker (QuotientHom (Q,N)) = @ ([#] N)
let N be normal SubLoop of Q; :: thesis: Ker (QuotientHom (Q,N)) = @ ([#] N)
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) )

proof

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

proof

assume A2: x in Ker (QuotientHom (Q,N)) ; :: thesis: x in @ ([#] N)
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: verum

end;

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

proof

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

proof

assume y in x * N ; :: thesis: y in (1. Q) * N
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: verum

end;

assume y in (1. Q) * N ; :: thesis: y in x * N
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 )

proof

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: ( h in Mlt (@ ([#] N)) & y = h . x )
thus h in Mlt (@ ([#] N)) by Th32; :: thesis: y = h . x
h . x = y1x1 * x by FUNCT_5:69
.= (y / x) * x by Th40
.= y ;
hence h . x = y ; :: thesis: verum

end;

hence y in x * N by Def39; :: thesis: verum

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: verum

end;

hence Ker (QuotientHom (Q,N)) = @ ([#] N) by SUBSET_1:3; :: thesis: verum