let J be set ; :: thesis: for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in J & i in dom A holds
A . i c= union (A,J)
let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT st i in J & i in dom A holds
A . i c= union (A,J)
let A be FinSequence of bool F; :: thesis: for i being Element of NAT st i in J & i in dom A holds
A . i c= union (A,J)
let i be Element of NAT ; :: thesis: ( i in J & i in dom A implies A . i c= union (A,J) )
assume A1: ( i in J & i in dom A ) ; :: thesis: A . i c= union (A,J)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in union (A,J) )
assume x in A . i ; :: thesis: x in union (A,J)
hence x in union (A,J) by A1, Def1; :: thesis: verum