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 st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
let Y be net of T; :: thesis: for J being net_set of the carrier of Y,T st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
let J be net_set of the carrier of Y,T; :: thesis: ( Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) implies Iterated J in NetUniv T )
assume that
A1: Y in NetUniv T and
A2: for i being Element of Y holds J . i in NetUniv T ; :: thesis: Iterated J in NetUniv T
RelStr(# the carrier of (Iterated J),the InternalRel of (Iterated J) #) = [:Y,(product J):] by Def16;
then A3: the carrier of (Iterated J) = [:the carrier of Y,the carrier of (product J):] by YELLOW_3:def 2;
A4: ex N being strict net of T st
( N = Y & the carrier of N in the_universe_of the carrier of T ) by A1, Def14;
then A5: dom (Carrier J) in the_universe_of the carrier of T by PARTFUN1:def 4;
rng (Carrier J) c= the_universe_of the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Carrier J) or x in the_universe_of the carrier of T )
assume x in rng (Carrier J) ; :: thesis: x in the_universe_of the carrier of T
then consider y being set such that
A6: y in dom (Carrier J) and
A7: (Carrier J) . y = x by FUNCT_1:def 5;
reconsider i = y as Element of Y by A6, PARTFUN1:def 4;
J . i in NetUniv T by A2;
then ex N being strict net of T st
( N = J . i & the carrier of N in the_universe_of the carrier of T ) by Def14;
hence x in the_universe_of the carrier of T by A7, Th9; :: thesis: verum

end;

then product (Carrier J) in the_universe_of the carrier of T by A5, Th5;
then the carrier of (product J) in the_universe_of the carrier of T by YELLOW_1:def 4;
then the carrier of (Iterated J) in the_universe_of the carrier of T by A3, A4, CLASSES2:67;
hence Iterated J in NetUniv T by Def14; :: thesis: verum