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

A2: now

let x be set ; :: thesis: ( x in meet (rng F1) implies for n being Nat st n in dom F1 holds
x in F1 . n )
assume A3: x in meet (rng F1) ; :: thesis: for n being Nat st n in dom F1 holds
x in F1 . n

now

let k be Nat; :: thesis: ( k in dom F1 implies x in F1 . k )
assume A4: k in dom F1 ; :: thesis: x in F1 . k
F1 . k in rng F1 by A4, FUNCT_1:12;
hence x in F1 . k by A3, SETFAM_1:def 1; :: thesis: verum

end;

hence for n being Nat st n in dom F1 holds
x in F1 . n ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( for n being Nat st n in dom F1 holds
x in F1 . n ) implies x in meet (rng F1) )
assume A5: for n being Nat st n in dom F1 holds
x in F1 . n ; :: thesis: x in meet (rng F1)

now

let Y be set ; :: thesis: ( Y in rng F1 implies x in Y )
assume Y in rng F1 ; :: thesis: x in Y
then consider n being set such that
A6: ( n in dom F1 & Y = F1 . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A6;
( n in dom F1 & Y = F1 . n ) by A6;
hence x in Y by A5; :: thesis: verum

end;

hence x in meet (rng F1) by A1, SETFAM_1:def 1; :: thesis: verum

end;

hence ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n ) by A2; :: thesis: verum