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
[#] (product J) 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
[#] (product J) 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
[#] (product J) 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 [#] (product J) c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } )
assume A1: [#] (J . i) c= union Fi ; :: thesis: [#] (product J) 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 [#] (product J) or f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } )
assume A2: f in [#] (product J) ; :: thesis: f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }
then reconsider f9 = f as Element of (product J) ;
f9 . i in [#] (J . i) ;
then consider Ai0 being set such that
A3: f9 . i in Ai0 and
A4: Ai0 in Fi by A1, TARSKI:def 4;
f9 in product (Carrier J) by A2, WAYBEL18:def 3;
then f9 in dom (proj ((Carrier J),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 A3, Th8;
then ( (proj (J,i)) " Ai0 in { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } & f9 in (proj (J,i)) " Ai0 ) by A5, FUNCT_1:def 7;
hence f in union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum } by TARSKI:def 4; :: thesis: verum