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
A2: ( n1 in NAT & n2 in NAT ) ;
thus addnat . n1,n2 = n1 + n2 by BINOP_2:def 23
.= addint . n1,n2 by A2, BINOP_2:def 20, NUMBERS:17
.= (addint || NAT ) . [n1,n2] by FUNCT_1:72
.= the multF of <NAT,+> . n1,n2 by A1, Th26, GR_CY_1:def 4 ; :: thesis: verum

end;

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