let T be non empty 1-sorted ; :: thesis: for Y being net of T
for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union { (rng the mapping of (J . i)) where i is Element of Y : verum }
let Y be net of T; :: thesis: for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union { (rng the mapping of (J . i)) where i is Element of Y : verum }
let J be net_set of the carrier of Y,T; :: thesis: rng the mapping of (Iterated J) c= union { (rng the mapping of (J . i)) where i is Element of Y : verum }
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the mapping of (Iterated J) or x in union { (rng the mapping of (J . i)) where i is Element of Y : verum } )
set X = { (rng the mapping of (J . i)) where i is Element of Y : verum } ;
assume x in rng the mapping of (Iterated J) ; :: thesis: x in union { (rng the mapping of (J . i)) where i is Element of Y : verum }
then consider y being set such that
A1: y in dom the mapping of (Iterated J) and
A2: the mapping of (Iterated J) . y = x by FUNCT_1:def 5;
y in the carrier of (Iterated J) by A1;
then y in [:the carrier of Y,(product (Carrier J)):] by Th35;
then consider y1 being Element of Y, y2 being Element of product (Carrier J) such that
A3: y = [y1,y2] by DOMAIN_1:9;
A4: y1 in the carrier of Y ;
y2 in product (Carrier J) ;
then A5: y2 in the carrier of (product J) by YELLOW_1:def 4;
y1 in dom (Carrier J) by A4, PARTFUN1:def 4;
then y2 . y1 in (Carrier J) . y1 by CARD_3:18;
then y2 . y1 in the carrier of (J . y1) by Th9;
then A6: y2 . y1 in dom the mapping of (J . y1) by FUNCT_2:def 1;
x = the mapping of (Iterated J) . y1,y2 by A2, A3
.= the mapping of (J . y1) . (y2 . y1) by A5, Def16 ;
then A7: x in rng the mapping of (J . y1) by A6, FUNCT_1:def 5;
reconsider y1 = y1 as Element of Y ;
rng the mapping of (J . y1) in { (rng the mapping of (J . i)) where i is Element of Y : verum } ;
hence x in union { (rng the mapping of (J . i)) where i is Element of Y : verum } by A7, TARSKI:def 4; :: thesis: verum