let x, b be non pair set ; :: thesis: the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
( the carrier of (CompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a]} & the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]} ) by Th27, Th31;
then the carrier of (BitCompStr (x,b)) = ({x,b} \/ {[<*x,b*>,xor2a]}) \/ ({x,b} \/ {[<*x,b*>,and2a]}) by CIRCCOMB:def 2
.= ({x,b} \/ ({x,b} \/ {[<*x,b*>,xor2a]})) \/ {[<*x,b*>,and2a]} by XBOOLE_1:4
.= (({x,b} \/ {x,b}) \/ {[<*x,b*>,xor2a]}) \/ {[<*x,b*>,and2a]} by XBOOLE_1:4
.= {x,b} \/ ({[<*x,b*>,xor2a]} \/ {[<*x,b*>,and2a]}) by XBOOLE_1:4
.= {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by ENUMSET1:1 ;
hence the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} ; :: thesis: verum