let x, b be non pair set ; :: thesis: the carrier of (IncrementStr x,b) = {x,b} \/ {[<*x,b*>,and2a ]}
set p = <*x,b*>;
rng <*x,b*> = {x,b} by FINSEQ_2:147;
hence the carrier of (IncrementStr x,b) = {x,b} \/ {[<*x,b*>,and2a ]} by CIRCCOMB:def 6; :: thesis: verum