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

consider o being BinOp of NAT such that

A1: 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 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