deffunc H₁( Nat, Nat) -> Element of omega = $1 gcd $2;
consider o being BinOp of NAT such that
A1: 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 gcd n
let m, n be Nat; :: thesis: o . (n,m) = n gcd m
( m in NAT & n in NAT ) by ORDINAL1:def 12;
hence o . (n,m) = n gcd m by A1; :: thesis: verum