When we start from the cardinality bijection definition of addition, we have to have a lot of lemmas built up already to show the additive identities, i.e. .the counting on identities.

2+0 = 2

We need to have the counting head segment {1,2} and we need to be able to do a bijection of it to some other set and then add the empty set and have the same bijection.

2+3′ = 5′

Now we need to do bijections from the counting head segment 3, {1,2,3} to some set and then add a unique element and do a bijection from the 3′ head segment, {1,2,3,4}.

We have to show that if we assume a bijection set up from

2+3=5

as the hypothesis step, that we can then work through the successor bijections required for the identity.

So we have two sets without common element in bijection to the counting head segments 2 and 3, and their union to the counting head segment 5.

Now we add a distinct element to the second set, get a new bijection to 3′, and show that the union of the new set has a bijection to head segment 5′.

A union B = C

A is in bijection to {1,2}, B to {1,2,3} and C to {1,2,3,4,5}

and then B’ is to {1,2,34} and C’ to {1,2,3,4,5,6}.

The lemmas and definitions to do this have to be developed.  This is what is needed to say we really have a working definition of addition by cardinality.  We have to be able to prove the right additive identities using the definition of addition. That requires a lot of lemmas to manage the bijections and to deal with the successor and the successor bijections.