let L be non empty 1-sorted ; :: thesis: for N being net of L

for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

let N be net of L; :: thesis: for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

let p be Function of N,N; :: thesis: ( N in NetUniv L implies N * p in NetUniv L )

assume N in NetUniv L ; :: thesis: N * p in NetUniv L

then A1: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

the carrier of (N * p) = the carrier of N by Th6;

hence N * p in NetUniv L by A1, YELLOW_6:def 11; :: thesis: verum

for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

let N be net of L; :: thesis: for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

let p be Function of N,N; :: thesis: ( N in NetUniv L implies N * p in NetUniv L )

assume N in NetUniv L ; :: thesis: N * p in NetUniv L

then A1: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

the carrier of (N * p) = the carrier of N by Th6;

hence N * p in NetUniv L by A1, YELLOW_6:def 11; :: thesis: verum