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)

proof

let z be set ; :: 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 ROUGH1;
then consider x being Element of X such that
A3: ( z = x & 1 <= #occurrences (x,A) ) ;
1 = 0 + 1 ;
then #occurrences (x,A) > 0 by A3, NAT_1:13;
then { i where i is Element of NAT : ( i in dom A & x in A . i ) } <> {} ;
then consider s being set 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
A4: ( s = i & i in dom A & x in A . i ) by A2;
thus z in Union A by A3, A4, CARD_5:2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Union A or z in ROUGH (A,1) )
assume A6: z in Union A ; :: thesis: z in ROUGH (A,1)
then consider s being set 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 1 c= #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 A6;
hence z in ROUGH (A,1) by A6, ROUGH1; :: thesis: verum