deffunc H₁( 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₁(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₁(m,n) by A3
.= m lcm n by A4, Def7, NEWTON:59 ; :: thesis: verum