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

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 <> {} )
;

end;

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;hence EXACTLY+- (B,0,0) = EXACTLY B ; :: thesis: verum

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)

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;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 or z in EXACTLY+- (B,0,0) )
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;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

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