set f = QuotientHom (Q,N);
thus (QuotientHom (Q,N)) . (1. Q) = 1. (Q _/_ N) by Def48; :: according to AIMLOOP:def 28,AIMLOOP:def 30 :: thesis: QuotientHom (Q,N) is quasi-homomorphic
let x, y be Element of Q; :: according to AIMLOOP:def 29 :: thesis: (QuotientHom (Q,N)) . (x * y) = ((QuotientHom (Q,N)) . x) * ((QuotientHom (Q,N)) . y)
reconsider xN = x * N as Element of Cosets N by Def41;
reconsider yN = y * N as Element of Cosets N by Def41;
(QuotientHom (Q,N)) . (x * y) = (x * y) * N by Def48
.= (x * N) * (y * N) by Def44
.= (Coset_Loop_Op N) . (xN,yN) by Def46
.= the multF of (Q _/_ N) . (((QuotientHom (Q,N)) . x),yN) by Def48
.= the multF of (Q _/_ N) . (((QuotientHom (Q,N)) . x),((QuotientHom (Q,N)) . y)) by Def48 ;
hence (QuotientHom (Q,N)) . (x * y) = ((QuotientHom (Q,N)) . x) * ((QuotientHom (Q,N)) . y) ; :: thesis: verum