let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
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 TopSpace-yielding ManySortedSet of ; :: 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 set ; :: 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 A3: f in the carrier of (product J) ;
reconsider f' = f as Element of (product J) by A2;
f' . i in [#] (J . i) ;
then consider Ai0 being set such that
A4: f' . i in Ai0 and
A5: Ai0 in Fi by A1, TARSKI:def 4;
reconsider Ai0 = Ai0 as Element of Fi by A5;
A6: (proj J,i) " Ai0 in { ((proj J,i) " Ai) where Ai is Element of Fi : verum } ;
f' in product (Carrier J) by A3, WAYBEL18:def 3;
then f' in dom (proj (Carrier J),i) by PRALG_3:def 2;
then A7: f' in dom (proj J,i) by WAYBEL18:def 4;
(proj J,i) . f' in Ai0 by A4, Th8;
then f' in (proj J,i) " Ai0 by A7, FUNCT_1:def 13;
hence f in union { ((proj J,i) " Ai) where Ai is Element of Fi : verum } by A6, TARSKI:def 4; :: thesis: verum