deffunc H₁( Element of Quot. I, Element of Quot. I) -> Element of Quot. I = qadd $1,$2;
consider F being BinOp of (Quot. I) such that
A1: for u, v being Element of Quot. I holds F . u,v = H₁(u,v) from BINOP_1:sch 4();
take F ; :: thesis: for u, v being Element of Quot. I holds F . u,v = qadd u,v
let u, v be Element of Quot. I; :: thesis: F . u,v = qadd u,v
thus F . u,v = qadd u,v by A1; :: thesis: verum