deffunc H₁( Element of NATPLUS , Element of NATPLUS ) -> Element of NATPLUS = @ ($1 gcd $2);
consider f being BinOp of NATPLUS such that
A1: for m, n being Element of NATPLUS holds f . m,n = H₁(m,n) from BINOP_1:sch 4();
take f ; :: thesis: for m, n being NatPlus holds f . m,n = m gcd n
let m, n be Element of NATPLUS ; :: thesis: f . m,n = m gcd n
A2: f . m,n = @ (m gcd n) by A1;
n > 0 by Def9;
hence f . m,n = m gcd n by A2, Def10, NEWTON:71; :: thesis: verum