let x be object ; :: thesis: for X being set

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

x in F1 . n ) by A2; :: thesis: verum

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 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 :: thesis: for x being object st ( for n being Nat st n in dom F1 holds

x in F1 . n ) holds

x in meet (rng F1)

x in F1 . n ) holds

x in meet (rng F1)

let x be object ; :: 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)

end;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 :: thesis: for Y being set st Y in rng F1 holds

x in Y

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

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 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: verum

end;assume Y in rng F1 ; :: thesis: x in Y

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: verum

now :: thesis: for x being object st x in meet (rng F1) holds

for n being Nat st n in dom F1 holds

x in F1 . n

hence
( x in meet (rng F1) iff for n being Nat st n in dom F1 holds for n being Nat st n in dom F1 holds

x in F1 . n

let x be object ; :: 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

x in F1 . n ; :: thesis: verum

end;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 :: thesis: for k being Nat st k in dom F1 holds

x in F1 . k

hence
for n being Nat st n in dom F1 holds x in F1 . k

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

x in F1 . n ; :: thesis: verum

x in F1 . n ) by A2; :: thesis: verum