set QN = Q _/_ N;
A1: for H being Element of (Q _/_ N) holds
( H * (1. (Q _/_ N)) = H & (1. (Q _/_ N)) * H = H )

proof

let H be Element of (Q _/_ N); :: thesis: ( H * (1. (Q _/_ N)) = H & (1. (Q _/_ N)) * H = H )
H in Cosets N ;
then consider x being Element of Q such that
A2: H = x * N by Def41;
A3: H * (1. (Q _/_ N)) = H

proof

reconsider H = H as Element of Cosets N ;
the multF of (Q _/_ N) . (H,(1. (Q _/_ N))) = H * ((1. Q) * N) by Def46
.= (x * (1. Q)) * N by A2, Def44
.= H by A2 ;
hence H * (1. (Q _/_ N)) = H ; :: thesis: verum

end;

(1. (Q _/_ N)) * H = H

proof

reconsider H = H as Element of Cosets N ;
the multF of (Q _/_ N) . ((1. (Q _/_ N)),H) = ((1. Q) * N) * H by Def46
.= ((1. Q) * x) * N by A2, Def44
.= H by A2 ;
hence (1. (Q _/_ N)) * H = H ; :: thesis: verum

end;

hence ( H * (1. (Q _/_ N)) = H & (1. (Q _/_ N)) * H = H ) by A3; :: thesis: verum

end;

A4: for H1, H2 being Element of (Q _/_ N) ex H3 being Element of (Q _/_ N) st H1 * H3 = H2

proof

let H1, H2 be Element of (Q _/_ N); :: thesis: ex H3 being Element of (Q _/_ N) st H1 * H3 = H2
H1 in Cosets N ;
then consider x being Element of Q such that
A5: H1 = x * N by Def41;
H2 in Cosets N ;
then consider y being Element of Q such that
A6: H2 = y * N by Def41;
reconsider H3 = (x \ y) * N as Element of (Q _/_ N) by Def41;
take H3 ; :: thesis: H1 * H3 = H2
the multF of (Q _/_ N) . (H1,H3) = (x * N) * ((x \ y) * N) by A5, Def46
.= (x * (x \ y)) * N by Def44
.= H2 by A6 ;
hence H1 * H3 = H2 ; :: thesis: verum

end;

A7: for H1, H2 being Element of (Q _/_ N) ex H3 being Element of (Q _/_ N) st H3 * H1 = H2

proof

let H1, H2 be Element of (Q _/_ N); :: thesis: ex H3 being Element of (Q _/_ N) st H3 * H1 = H2
H1 in Cosets N ;
then consider x being Element of Q such that
A8: H1 = x * N by Def41;
H2 in Cosets N ;
then consider y being Element of Q such that
A9: H2 = y * N by Def41;
reconsider H3 = (y / x) * N as Element of (Q _/_ N) by Def41;
take H3 ; :: thesis: H3 * H1 = H2
the multF of (Q _/_ N) . (H3,H1) = ((y / x) * N) * (x * N) by A8, Def46
.= ((y / x) * x) * N by Def44
.= H2 by A9 ;
hence H3 * H1 = H2 ; :: thesis: verum

end;

for H1 being Element of (Q _/_ N) holds H1 is left_mult-cancelable

proof

let H1 be Element of (Q _/_ N); :: thesis: H1 is left_mult-cancelable
for H2, H3 being Element of (Q _/_ N) st H1 * H2 = H1 * H3 holds
H2 = H3

proof

let H2, H3 be Element of (Q _/_ N); :: thesis: ( H1 * H2 = H1 * H3 implies H2 = H3 )
H1 in Cosets N ;
then consider x being Element of Q such that
A10: H1 = x * N by Def41;
H2 in Cosets N ;
then consider y being Element of Q such that
A11: H2 = y * N by Def41;
H3 in Cosets N ;
then consider z being Element of Q such that
A12: H3 = z * N by Def41;
assume A13: H1 * H2 = H1 * H3 ; :: thesis: H2 = H3
(x * N) * (y * N) = H1 * H2 by A10, A11, Def46
.= (x * N) * (z * N) by A10, A12, A13, Def46 ;
hence H2 = H3 by A11, A12, Def44; :: thesis: verum

end;

hence H1 is left_mult-cancelable by ALGSTR_0:def 20; :: thesis: verum

end;

then A14: Q _/_ N is left_mult-cancelable by ALGSTR_0:def 23;
for H1 being Element of (Q _/_ N) holds H1 is right_mult-cancelable

proof

let H1 be Element of (Q _/_ N); :: thesis: H1 is right_mult-cancelable
let H2, H3 be Element of (Q _/_ N); :: according to ALGSTR_0:def 21 :: thesis: ( not H2 * H1 = H3 * H1 or H2 = H3 )
H1 in Cosets N ;
then consider x being Element of Q such that
A15: H1 = x * N by Def41;
H2 in Cosets N ;
then consider y being Element of Q such that
A16: H2 = y * N by Def41;
H3 in Cosets N ;
then consider z being Element of Q such that
A17: H3 = z * N by Def41;
assume A18: H2 * H1 = H3 * H1 ; :: thesis: H2 = H3
(y * N) * (x * N) = H2 * H1 by A15, A16, Def46
.= (z * N) * (x * N) by A18, A15, A17, Def46 ;
hence H2 = H3 by A16, A17, Def44; :: thesis: verum

end;

then Q _/_ N is right_mult-cancelable by ALGSTR_0:def 24;
hence ( Q _/_ N is well-unital & Q _/_ N is invertible & Q _/_ N is mult-cancelable ) by A1, A7, ALGSTR_1:def 6, A4, A14; :: thesis: verum