let F be non empty set ; :: thesis: for f being non-empty FinSequence of bool F
for i being Element of NAT st i in dom f holds
f . i <> {}
let f be non-empty FinSequence of bool F; :: thesis: for i being Element of NAT st i in dom f holds
f . i <> {}
let i be Element of NAT ; :: thesis: ( i in dom f implies f . i <> {} )
assume A1: i in dom f ; :: thesis: f . i <> {}
assume f . i = {} ; :: thesis: contradiction
then {} in rng f by A1, FUNCT_1:3;
hence contradiction by RELAT_1:def 9; :: thesis: verum