let Y be ref-finite ConstructorDB ; 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; EXACTLY+- (B,0,0) = EXACTLY B
per cases
( the carrier of Y = {} or the carrier of Y <> {} )
;
suppose A1:
the
carrier of
Y <> {}
;
EXACTLY+- (B,0,0) = EXACTLY Bthen 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
XBOOLE_0:def 10 EXACTLY B c= EXACTLY+- (B,0,0)let z be
object ;
TARSKI:def 3 ( not z in EXACTLY B or z in EXACTLY+- (B,0,0) )assume
z in EXACTLY B
;
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;
verum end; end;