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 Th32, Th40;
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:41 ;
hence the carrier of (BitCompStr x,b) = {x,b} \/ {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} ; :: thesis: verum