let T be non empty 1-sorted ; 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; 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; rng the mapping of (Iterated J) c= union { (rng the mapping of (J . i)) where i is Element of Y : verum }
let x be object ; TARSKI:def 3 ( 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)
; x in union { (rng the mapping of (J . i)) where i is Element of Y : verum }
then consider y being object such that
A1:
y in dom the mapping of (Iterated J)
and
A2:
the mapping of (Iterated J) . y = x
by FUNCT_1:def 3;
y in the carrier of (Iterated J)
by A1;
then
y in [: the carrier of Y,(product (Carrier J)):]
by Th26;
then consider y1 being Element of Y, y2 being Element of product (Carrier J) such that
A3:
y = [y1,y2]
by DOMAIN_1:1;
y1 in the carrier of Y
;
then
y1 in dom (Carrier J)
by PARTFUN1:def 2;
then
y2 . y1 in (Carrier J) . y1
by CARD_3:9;
then
y2 . y1 in the carrier of (J . y1)
by Th2;
then A4:
y2 . y1 in dom the mapping of (J . y1)
by FUNCT_2:def 1;
y2 in product (Carrier J)
;
then A5:
y2 in the carrier of (product J)
by YELLOW_1:def 4;
x =
the mapping of (Iterated J) . (y1,y2)
by A2, A3
.=
the mapping of (J . y1) . (y2 . y1)
by A5, Def13
;
then A6:
x in rng the mapping of (J . y1)
by A4, FUNCT_1:def 3;
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 A6, TARSKI:def 4; verum