let b be BinOp of NAT; :: thesis: ( b = addnat iff b = the multF of <NAT,+> )
A1: the carrier of <NAT,+> = NAT by Def27;

now

let n1, n2 be Element of NAT ; :: thesis: addnat . (n1,n2) = the multF of <NAT,+> . (n1,n2)
thus addnat . (n1,n2) = n1 + n2 by BINOP_2:def 23
.= addint . (n1,n2) by BINOP_2:def 20
.= (addint || NAT) . [n1,n2] by FUNCT_1:49
.= the multF of <NAT,+> . (n1,n2) by A1, Th26, GR_CY_1:def 3 ; :: thesis: verum

end;

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