let X be set ; :: thesis: for F1 being FinSequence of bool X

for x being object 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: for x being object st F1 <> {} holds

( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k )

let x be object ; :: thesis: ( F1 <> {} implies ( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k ) )

A1: for n being Nat st n in dom F1 holds

X \ ((Complement F1) . n) = F1 . n

x in F1 . k )

then A4: dom F1 <> {} by RELAT_1:41;

A5: ( ( 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 )

then A12: ( 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 ) ) ) by Th49;

( x in (Union (Complement F1)) ` iff x in X \ (Union (Complement F1)) ) by SUBSET_1:def 4;

hence ( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k ) by A3, A12, A5, Def6, XBOOLE_0:def 5; :: thesis: verum

for x being object 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: for x being object st F1 <> {} holds

( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k )

let x be object ; :: thesis: ( F1 <> {} implies ( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k ) )

A1: for n being Nat st n in dom F1 holds

X \ ((Complement F1) . n) = F1 . n

proof

assume A3:
F1 <> {}
; :: thesis: ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
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 A2: n in dom (Complement F1) by Th50;

X \ ((Complement F1) . n) = ((Complement F1) . n) ` by SUBSET_1:def 4

.= ((F1 . n) `) ` by A2, Def5

.= F1 . n ;

hence X \ ((Complement F1) . n) = F1 . n ; :: thesis: verum

end;assume n in dom F1 ; :: thesis: X \ ((Complement F1) . n) = F1 . n

then A2: n in dom (Complement F1) by Th50;

X \ ((Complement F1) . n) = ((Complement F1) . n) ` by SUBSET_1:def 4

.= ((F1 . n) `) ` by A2, Def5

.= F1 . n ;

hence X \ ((Complement F1) . n) = F1 . n ; :: thesis: verum

x in F1 . k )

then A4: dom F1 <> {} by RELAT_1:41;

A5: ( ( 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

x in F1 . n ; :: thesis: ( x in X & ( for n being Nat st n in dom F1 holds

not x in (Complement F1) . n ) )

hence ( x in X & ( for n being Nat st n in dom F1 holds

not x in (Complement F1) . n ) ) by A10; :: thesis: verum

end;

dom (Complement F1) = dom F1
by Th50;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 A9:
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 that

A6: x in X and

A7: 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 A8: n in dom F1 ; :: thesis: x in F1 . n

not x in (Complement F1) . n by A7, A8;

then x in X \ ((Complement F1) . n) by A6, XBOOLE_0:def 5;

hence x in F1 . n by A1, A8; :: thesis: verum

end;A6: x in X and

A7: 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 A8: n in dom F1 ; :: thesis: x in F1 . n

not x in (Complement F1) . n by A7, A8;

then x in X \ ((Complement F1) . n) by A6, XBOOLE_0:def 5;

hence x in F1 . n by A1, A8; :: thesis: verum

x in F1 . n ; :: thesis: ( x in X & ( for n being Nat st n in dom F1 holds

not x in (Complement F1) . n ) )

A10: now :: thesis: for n being Element of NAT st n in dom F1 holds

( x in X & not x in (Complement F1) . n )

ex a being object st a in dom F1
by A4, XBOOLE_0:def 1;( x in X & not x in (Complement F1) . n )

let n be Element of NAT ; :: thesis: ( n in dom F1 implies ( x in X & not x in (Complement F1) . n ) )

assume A11: n in dom F1 ; :: thesis: ( x in X & not x in (Complement F1) . n )

x in F1 . n by A9, A11;

then x in X \ ((Complement F1) . n) by A1, A11;

hence ( x in X & not x in (Complement F1) . n ) by XBOOLE_0:def 5; :: thesis: verum

end;assume A11: n in dom F1 ; :: thesis: ( x in X & not x in (Complement F1) . n )

x in F1 . n by A9, A11;

then x in X \ ((Complement F1) . n) by A1, A11;

hence ( x in X & not x in (Complement F1) . n ) by XBOOLE_0:def 5; :: thesis: verum

hence ( x in X & ( for n being Nat st n in dom F1 holds

not x in (Complement F1) . n ) ) by A10; :: thesis: verum

then A12: ( 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 ) ) ) by Th49;

( x in (Union (Complement F1)) ` iff x in X \ (Union (Complement F1)) ) by SUBSET_1:def 4;

hence ( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k ) by A3, A12, A5, Def6, XBOOLE_0:def 5; :: thesis: verum