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

A2: 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 A3: 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
A4: n in dom F1 and
A5: Y = F1 . n by FUNCT_1:def 3;
thus x in Y by A3, A4, A5; :: thesis: verum

end;

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

end;

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 A6: 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 k in dom F1 ; :: thesis: x in F1 . k
then F1 . k in rng F1 by FUNCT_1:3;
hence x in F1 . k by A6, 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;

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