deffunc H₁( Element of Q) -> Subset of Q = $1 * N;
consider f being Function of Q,(bool the carrier of Q) such that
A1: for x being Element of Q holds f . x = H₁(x) from FUNCT_2:sch 4();
A2: dom f = the carrier of Q by FUNCT_2:def 1;
A3: rng f c= the carrier of (Q _/_ N)

proof

let H be object ; :: according to TARSKI:def 3 :: thesis: ( not H in rng f or H in the carrier of (Q _/_ N) )
assume H in rng f ; :: thesis: H in the carrier of (Q _/_ N)
then consider x being object such that
A4: ( x in dom f & H = f . x ) by FUNCT_1:def 3;
reconsider x = x as Element of Q by A4, FUNCT_2:def 1;
H = x * N by A1, A4;
hence H in the carrier of (Q _/_ N) by Def41; :: thesis: verum

end;

reconsider f = f as Function of Q,(Q _/_ N) by FUNCT_2:2, A2, A3;
take f ; :: thesis: for x being Element of Q holds f . x = x * N
thus for x being Element of Q holds f . x = x * N by A1; :: thesis: verum