deffunc H_{1}( 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_{1}(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

consider o being BinOp of NAT such that

A4: for a, b being Element of NAT holds o . (a,b) = H

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