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 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;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Union A or z in 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