deffunc H_{1}( NatPlus, NatPlus) -> NatPlus = @ ($1 lcm $2);

consider f being BinOp of NATPLUS such that

A3: 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 lcm n

let m, n be NatPlus; :: thesis: f . (m,n) = m lcm n

A4: ( m > 0 & n > 0 ) by Def6;

thus f . (m,n) = H_{1}(m,n)
by A3

.= m lcm n by A4, Def7, NEWTON:59 ; :: thesis: verum

consider f being BinOp of NATPLUS such that

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

take f ; :: thesis: for m, n being NatPlus holds f . (m,n) = m lcm n

let m, n be NatPlus; :: thesis: f . (m,n) = m lcm n

A4: ( m > 0 & n > 0 ) by Def6;

thus f . (m,n) = H

.= m lcm n by A4, Def7, NEWTON:59 ; :: thesis: verum