let F be set ; :: thesis: for A being FinSequence of bool F
for J being set holds union (A,J) c= F
let A be FinSequence of bool F; :: thesis: for J being set holds union (A,J) c= F
let J be set ; :: thesis: union (A,J) c= F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A,J) or x in F )
assume x in union (A,J) ; :: thesis: x in F
then consider j being set such that
j in J and
A1: j in dom A and
A2: x in A . j by Def1;
( rng A c= bool F & A . j in rng A ) by A1, FINSEQ_1:def 4, FUNCT_1:3;
hence x in F by A2; :: thesis: verum