let b be BinOp of NAT; :: thesis: ( b = addnat iff b = the multF of <NAT,+> )
A1: the carrier of <NAT,+> = NAT by Def27;
now :: thesis: for n1, n2 being Element of NAT holds addnat . (n1,n2) = the multF of <NAT,+> . (n1,n2)
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, Th24, GR_CY_1:def 3 ; :: thesis: verum
end;
hence ( b = addnat iff b = the multF of <NAT,+> ) by A1, BINOP_1:2; :: thesis: verum