let x be object ; :: thesis:
let X be set ; :: thesis:
let F1 be FinSequence of bool X; :: thesis:
assume F1 <> {} ; :: thesis:
then A1: rng F1 <> {} by RELAT_1:41;

A2: now :: thesis:

let x be object ; :: thesis:
assume A3: for n being Nat st n in dom F1 holds
x in F1 . n ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in rng F1 ; :: thesis:
then consider n being object 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:

end;

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

end;

now :: thesis:

let x be object ; :: thesis:
assume A6: x in meet (rng F1) ; :: thesis:

now :: thesis:

let k be Nat; :: thesis:
assume k in dom F1 ; :: thesis:
then F1 . k in rng F1 by FUNCT_1:3;
hence x in F1 . k by A6, SETFAM_1:def 1; :: thesis:

end;

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

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: