let T be non empty 1-sorted ; :: thesis: for N being net of T
for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
let N be net of T; :: thesis: for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
let J be net_set of the carrier of N,T; :: thesis: the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:N,(product J):] by Def13;
hence the carrier of (Iterated J) = [: the carrier of N, the carrier of (product J):] by YELLOW_3:def 2
.= [: the carrier of N,(product (Carrier J)):] by YELLOW_1:def 4 ;
:: thesis: verum