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:127;
hence the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]} by CIRCCOMB:def 6; :: thesis: verum