deffunc H₁( Element of Cosets N, Element of Cosets N) -> Subset of Q = $1 * $2;
A1: for H1, H2 being Element of Cosets N holds H₁(H1,H2) in Cosets N

proof

let H1, H2 be Element of Cosets N; :: thesis: H₁(H1,H2) in Cosets N
consider x being Element of Q such that
A2: H1 = x * N by Def41;
consider y being Element of Q such that
A3: H2 = y * N by Def41;
H₁(H1,H2) = (x * y) * N by Def44, A2, A3;
hence H₁(H1,H2) in Cosets N by Def41; :: thesis: verum

end;

consider g being Function of [:(Cosets N),(Cosets N):],(Cosets N) such that
A4: for H1, H2 being Element of Cosets N holds g . (H1,H2) = H₁(H1,H2) from FUNCT_7:sch 1(A1);
take g ; :: thesis: for H1, H2 being Element of Cosets N holds g . (H1,H2) = H1 * H2
thus for H1, H2 being Element of Cosets N holds g . (H1,H2) = H1 * H2 by A4; :: thesis: verum