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