deffunc H₁( Nat, Nat) -> Element of omega = $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 n, m being Nat holds o . (m,n) = m lcm n
let m, n be Nat; :: thesis: o . (n,m) = n lcm m
( m in NAT & n in NAT ) by ORDINAL1:def 12;
hence o . (n,m) = n lcm m by A4; :: thesis: verum