deffunc H_{1}( 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_{1}(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

consider f being BinOp of NATPLUS such that

A1: for m, n being NatPlus holds f . (m,n) = H

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