deffunc H₁( Nat, Nat) -> Element of NAT = $1 lcm $2;
consider o being BinOp of NAT such that
A4: for a, b being Element of NAT holds o . a,b = H₁(a,b) from BINOP_1:sch 4();
take o ; :: thesis: for m, n being Nat holds o . m,n = m lcm n
let m, n be Nat; :: thesis: o . m,n = m lcm n
( m in NAT & n in NAT ) by ORDINAL1:def 13;
hence o . m,n = m lcm n by A4; :: thesis: verum