deffunc H₁( Element of NATPLUS , Element of NATPLUS ) -> Element of NATPLUS = @ ((@ $1) lcm (@ $2));
consider f being BinOp of NATPLUS such that
A3: 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 lcm n
let m, n be Element of NATPLUS ; :: thesis: f . m,n = m lcm n
( @ n = n & @ m = m ) ;
then A4: f . m,n = @ (m lcm n) by A3;
( m > 0 & n > 0 ) by Def9;
hence f . m,n = m lcm n by A4, Def10, NEWTON:73; :: thesis: verum