let F be non empty finite set ; :: thesis: for A being non-empty FinSequence of bool F
for i being Element of NAT
for B being Singlification of A,i st i in dom A holds
B . i <> {}
let A be non-empty FinSequence of bool F; :: thesis: for i being Element of NAT
for B being Singlification of A,i st i in dom A holds
B . i <> {}
let i be Element of NAT ; :: thesis: for B being Singlification of A,i st i in dom A holds
B . i <> {}
let B be Singlification of A,i; :: thesis: ( i in dom A implies B . i <> {} )
assume A1: i in dom A ; :: thesis: B . i <> {}
then A . i <> {} by Th2;
hence B . i <> {} by A1, Def7, CARD_1:27; :: thesis: verum