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
A3: rng (Carrier J) c= the_universe_of the carrier of T

proof

let x be object ; :: 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 object such that
A4: y in dom (Carrier J) and
A5: (Carrier J) . y = x by FUNCT_1:def 3;
reconsider i = y as Element of Y by A4;
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 Def11;
hence x in the_universe_of the carrier of T by A5, Th2; :: thesis: verum

end;

RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:Y,(product J):] by Def13;
then A6: the carrier of (Iterated J) = [: the carrier of Y, the carrier of (product J):] by YELLOW_3:def 2;
A7: ex N being strict net of T st
( N = Y & the carrier of N in the_universe_of the carrier of T ) by A1, Def11;
then dom (Carrier J) in the_universe_of the carrier of T by PARTFUN1:def 2;
then product (Carrier J) in the_universe_of the carrier of T by A3, Th1;
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 A6, A7, CLASSES2:61;
hence Iterated J in NetUniv T by Def11; :: thesis: verum