let X, x be set ; :: thesis: for F1 being FinSequence of bool X st F1 <> {} holds
( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )
let F1 be FinSequence of bool X; :: thesis: ( F1 <> {} implies ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k ) )
assume A1: F1 <> {} ; :: thesis: ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )
then A2: dom F1 <> {} by RELAT_1:64;
A3: for n being Nat st n in dom F1 holds
X \ ((Complement F1) . n) = F1 . n

proof

let n be Nat; :: thesis: ( n in dom F1 implies X \ ((Complement F1) . n) = F1 . n )
assume n in dom F1 ; :: thesis: X \ ((Complement F1) . n) = F1 . n
then A4: n in dom (Complement F1) by Th55;
X \ ((Complement F1) . n) = ((Complement F1) . n) ` by SUBSET_1:def 5
.= ((F1 . n) ` ) ` by A4, Def8
.= F1 . n ;
hence X \ ((Complement F1) . n) = F1 . n ; :: thesis: verum

end;

A5: ( x in (Union (Complement F1)) ` iff x in X \ (Union (Complement F1)) ) by SUBSET_1:def 5;
A6: ( x in X & not x in Union (Complement F1) iff ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) )

proof

A7: dom (Complement F1) = dom F1 by Th55;
hence ( x in X & not x in Union (Complement F1) implies ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) ) by Th54; :: thesis: ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) implies ( x in X & not x in Union (Complement F1) ) )
thus ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) implies ( x in X & not x in Union (Complement F1) ) ) by A7, Th54; :: thesis: verum

end;

( ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) iff for n being Nat st n in dom F1 holds
x in F1 . n )

proof

hereby :: thesis: ( ( for n being Nat st n in dom F1 holds
x in F1 . n ) implies ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) )

assume A8: ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) ; :: thesis: for n being Nat st n in dom F1 holds
x in F1 . n
let n be Nat; :: thesis: ( n in dom F1 implies x in F1 . n )
assume A9: n in dom F1 ; :: thesis: x in F1 . n
( x in X & not x in (Complement F1) . n ) by A8, A9;
then x in X \ ((Complement F1) . n) by XBOOLE_0:def 5;
hence x in F1 . n by A3, A9; :: thesis: verum

end;

assume A10: for n being Nat st n in dom F1 holds
x in F1 . n ; :: thesis: ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) )

A11: now

let n be Element of NAT ; :: thesis: ( n in dom F1 implies ( x in X & not x in (Complement F1) . n ) )
assume A12: n in dom F1 ; :: thesis: ( x in X & not x in (Complement F1) . n )
x in F1 . n by A10, A12;
then x in X \ ((Complement F1) . n) by A3, A12;
hence ( x in X & not x in (Complement F1) . n ) by XBOOLE_0:def 5; :: thesis: verum

end;

consider a being set such that
A13: a in dom F1 by A2, XBOOLE_0:def 1;
thus ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) by A11, A13; :: thesis: verum

end;

hence ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k ) by A1, A5, A6, Def9, XBOOLE_0:def 5; :: thesis: verum