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