let b be BinOp of NAT; ( b = multnat iff b = the multF of <NAT,*> )
A1:
the carrier of <NAT,*> = NAT
by Def31;
now for n1, n2 being Element of NAT holds multnat . (n1,n2) = the multF of <NAT,*> . (n1,n2)let n1,
n2 be
Element of
NAT ;
multnat . (n1,n2) = the multF of <NAT,*> . (n1,n2)thus multnat . (
n1,
n2) =
n1 * n2
by BINOP_2:def 24
.=
multreal . (
n1,
n2)
by BINOP_2:def 11
.=
(multreal || NAT) . [n1,n2]
by FUNCT_1:49
.=
the
multF of
<NAT,*> . (
n1,
n2)
by A1, Th24
;
verum end;
hence
( b = multnat iff b = the multF of <NAT,*> )
by A1, BINOP_1:2; verum