let b be BinOp of NAT; :: thesis: ( b = multnat iff b = the multF of <NAT,*> )
A1: the carrier of <NAT,*> = NAT by Def31;

now :: thesis: for n1, n2 being Element of NAT holds multnat . (n1,n2) = the multF of <NAT,*> . (n1,n2)

let n1, n2 be Element of NAT ; :: thesis: 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 ; :: thesis: verum

end;

hence ( b = multnat iff b = the multF of <NAT,*> ) by A1, BINOP_1:2; :: thesis: verum