deffunc H₁( Element of Quot. I, Element of Quot. I) -> Element of Quot. I = qmult ($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) = qmult (u,v)
let u, v be Element of Quot. I; :: thesis: F . (u,v) = qmult (u,v)
thus F . (u,v) = qmult (u,v) by A1; :: thesis: verum