let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] () c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] () c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }

let i be Element of I; :: thesis: for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] () c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }

let Fi be non empty Subset-Family of (J . i); :: thesis: ( [#] (J . i) c= union Fi implies [#] () c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } )
assume A1: [#] (J . i) c= union Fi ; :: thesis: [#] () c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in [#] () or f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } )
assume A2: f in [#] () ; :: thesis: f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }
then reconsider f9 = f as Element of () ;
f9 . i in [#] (J . i) ;
then consider Ai0 being set such that
A3: f9 . i in Ai0 and
A4: Ai0 in Fi by ;
f9 in product () by ;
then f9 in dom (proj ((),i)) by CARD_3:def 16;
then A5: f9 in dom (proj (J,i)) by WAYBEL18:def 4;
reconsider Ai0 = Ai0 as Element of Fi by A4;
(proj (J,i)) . f9 in Ai0 by ;
then ( (proj (J,i)) " Ai0 in { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } & f9 in (proj (J,i)) " Ai0 ) by ;
hence f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } by TARSKI:def 4; :: thesis: verum