let X be set ; :: thesis: for A being FinSequence of bool X holds ROUGH (A,1) = Union A

let A be FinSequence of bool X; :: thesis: ROUGH (A,1) = Union A

thus ROUGH (A,1) c= Union A :: according to XBOOLE_0:def 10 :: thesis: Union A c= ROUGH (A,1)

assume A4: z in Union A ; :: thesis: z in ROUGH (A,1)

then consider s being object such that

A5: ( s in dom A & z in A . s ) by CARD_5:2;

s in { i where i is Element of NAT : ( i in dom A & z in A . i ) } by A5;

then card {s} c= #occurrences (z,A) by CARD_1:11, ZFMISC_1:31;

then Segm 1 c= Segm (#occurrences (z,A)) by CARD_1:30;

then 1 <= #occurrences (z,A) by NAT_1:39;

then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by A4;

hence z in ROUGH (A,1) by A4, Def24; :: thesis: verum

let A be FinSequence of bool X; :: thesis: ROUGH (A,1) = Union A

thus ROUGH (A,1) c= Union A :: according to XBOOLE_0:def 10 :: thesis: Union A c= ROUGH (A,1)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Union A or z in ROUGH (A,1) )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,1) or z in Union A )

assume z in ROUGH (A,1) ; :: thesis: z in Union A

then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by Def24;

then consider x being Element of X such that

A1: ( z = x & 1 <= #occurrences (x,A) ) ;

1 = 0 + 1 ;

then #occurrences (x,A) > 0 by A1, NAT_1:13;

then { i where i is Element of NAT : ( i in dom A & x in A . i ) } <> {} ;

then consider s being object such that

A2: s in { i where i is Element of NAT : ( i in dom A & x in A . i ) } by XBOOLE_0:def 1;

consider i being Element of NAT such that

A3: ( s = i & i in dom A & x in A . i ) by A2;

thus z in Union A by A1, A3, CARD_5:2; :: thesis: verum

end;assume z in ROUGH (A,1) ; :: thesis: z in Union A

then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by Def24;

then consider x being Element of X such that

A1: ( z = x & 1 <= #occurrences (x,A) ) ;

1 = 0 + 1 ;

then #occurrences (x,A) > 0 by A1, NAT_1:13;

then { i where i is Element of NAT : ( i in dom A & x in A . i ) } <> {} ;

then consider s being object such that

A2: s in { i where i is Element of NAT : ( i in dom A & x in A . i ) } by XBOOLE_0:def 1;

consider i being Element of NAT such that

A3: ( s = i & i in dom A & x in A . i ) by A2;

thus z in Union A by A1, A3, CARD_5:2; :: thesis: verum

assume A4: z in Union A ; :: thesis: z in ROUGH (A,1)

then consider s being object such that

A5: ( s in dom A & z in A . s ) by CARD_5:2;

s in { i where i is Element of NAT : ( i in dom A & z in A . i ) } by A5;

then card {s} c= #occurrences (z,A) by CARD_1:11, ZFMISC_1:31;

then Segm 1 c= Segm (#occurrences (z,A)) by CARD_1:30;

then 1 <= #occurrences (z,A) by NAT_1:39;

then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by A4;

hence z in ROUGH (A,1) by A4, Def24; :: thesis: verum