let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,0,0) = EXACTLY B
let B be FinSequence of the Constrs of Y; :: thesis: EXACTLY+- (B,0,0) = EXACTLY B

per cases ( the carrier of Y = {} or the carrier of Y <> {} ) ;

suppose the carrier of Y = {} ; :: thesis: EXACTLY+- (B,0,0) = EXACTLY B

then ( EXACTLY+- (B,0,0) = {} & EXACTLY B = {} ) ;
hence EXACTLY+- (B,0,0) = EXACTLY B ; :: thesis: verum

end;

suppose A0: the carrier of Y <> {} ; :: thesis: EXACTLY+- (B,0,0) = EXACTLY B

then A1: EXACTLY+- (B,0,0) = { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) } by DefExactlyPlusMinus;
A2: EXACTLY B = { y where y is Element of Y : y ref = rng B } by A0, DefExactly;
thus EXACTLY+- (B,0,0) c= EXACTLY B :: according to XBOOLE_0:def 10 :: thesis: EXACTLY B c= EXACTLY+- (B,0,0)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY+- (B,0,0) or z in EXACTLY B )
assume z in EXACTLY+- (B,0,0) ; :: thesis: z in EXACTLY B
then consider y being Element of Y such that
A3: ( z = y & card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) by A1;
( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A3, NAT_1:3;
then ( y ref c= rng B & rng B c= y ref ) by XBOOLE_1:37;
then y ref = rng B by XBOOLE_0:def 10;
hence z in EXACTLY B by A3, A2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in EXACTLY B or z in EXACTLY+- (B,0,0) )
assume z in EXACTLY B ; :: thesis: z in EXACTLY+- (B,0,0)
then consider y being Element of Y such that
A4: ( z = y & y ref = rng B ) by A2;
( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A4, XBOOLE_1:37;
then ( card ((y ref) \ (rng B)) = 0 & card ((rng B) \ (y ref)) = 0 ) ;
hence z in EXACTLY+- (B,0,0) by A1, A4; :: thesis: verum

end;

end;