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

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