deffunc H₁( NatPlus, NatPlus) -> NatPlus = @ ($1 gcd $2);
consider f being BinOp of NATPLUS such that
A1: for m, n being 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 NatPlus; :: thesis: f . (m,n) = m gcd n
A2: f . (m,n) = @ (m gcd n) by A1;
n > 0 by Def6;
hence f . (m,n) = m gcd n by A2, Def7, NEWTON:58; :: thesis: verum