let b be BinOp of NAT ; :: thesis: ( b = multnat iff b = the multF of <NAT,*> )
A1:
the carrier of <NAT,*> = NAT
by Def31;
now let n1,
n2 be
Element of
NAT ;
:: thesis: multnat . n1,n2 = the multF of <NAT,*> . n1,n2thus 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:72
.=
the
multF of
<NAT,*> . n1,
n2
by A1, Th26
;
:: thesis: verum end;
hence
( b = multnat iff b = the multF of <NAT,*> )
by A1, BINOP_1:2; :: thesis: verum