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 A1: the carrier of Y <> {} ; :: thesis: EXACTLY+- (B,0,0) = EXACTLY B
then A2: EXACTLY+- (B,0,0) = { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) } by Def36;
A3: EXACTLY B = { y where y is Element of Y : y ref = rng B } by A1, Def33;
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 object ; :: 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
A4: ( z = y & card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) by A2;
( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A4, NAT_1:3;
then ( y ref c= rng B & rng B c= y ref ) by XBOOLE_1:37;
then y ref = rng B ;
hence z in EXACTLY B by A4, A3; :: thesis: verum
end;
let z be object ; :: 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
A5: ( z = y & y ref = rng B ) by A3;
( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A5, XBOOLE_1:37;
then ( card ((y ref) \ (rng B)) = 0 & card ((rng B) \ (y ref)) = 0 ) ;
hence z in EXACTLY+- (B,0,0) by A2, A5; :: thesis: verum
end;
end;