let X be set ; :: thesis: for n being Nat
for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n)
let n be Nat; :: thesis: for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n)
let A be FinSequence of bool X; :: thesis: ROUGH (A,n,(len A)) = ROUGH (A,n)
thus ROUGH (A,n,(len A)) c= ROUGH (A,n) :: according to XBOOLE_0:def 10 :: thesis: ROUGH (A,n) c= ROUGH (A,n,(len A))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,n,(len A)) or z in ROUGH (A,n) )
assume A1: z in ROUGH (A,n,(len A)) ; :: thesis: z in ROUGH (A,n)
then z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= len A ) } by Def25;
then ex x being Element of X st
( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= len A ) ;
then z in { x where x is Element of X : n <= #occurrences (x,A) } ;
hence z in ROUGH (A,n) by A1, Def24; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,n) or z in ROUGH (A,n,(len A)) )
assume A2: z in ROUGH (A,n) ; :: thesis: z in ROUGH (A,n,(len A))
then z in { x where x is Element of X : n <= #occurrences (x,A) } by Def24;
then consider x being Element of X such that
A3: ( z = x & n <= #occurrences (x,A) ) ;
#occurrences (x,A) <= len A by Th54;
then z in { x1 where x1 is Element of X : ( n <= #occurrences (x1,A) & #occurrences (x1,A) <= len A ) } by A3;
hence z in ROUGH (A,n,(len A)) by A2, Def25; :: thesis: verum