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 set ; :: 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
A1: ( j in J & j in dom A & x in A . j ) by Def1;
A2: rng A c= bool F by FINSEQ_1:def 4;
A . j in rng A by A1, FUNCT_1:12;
hence x in F by A1, A2; :: thesis: verum