let X be set ; :: thesis: for T being 1-sorted
for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
let T be 1-sorted ; :: thesis: for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
let F be ManySortedSet of X; :: thesis: ( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
A1: dom F = X by PARTFUN1:def 2;

hereby :: thesis: ( ( for i being set st i in X holds
F . i is net of T ) implies F is net_set of X,T )

assume A2: F is net_set of X,T ; :: thesis: for i being set st i in X holds
F . i is net of T
let i be set ; :: thesis: ( i in X implies F . i is net of T )
assume i in X ; :: thesis: F . i is net of T
then i in dom F by PARTFUN1:def 2;
then F . i in rng F by FUNCT_1:def 3;
hence F . i is net of T by A2, Def15; :: thesis: verum

end;

assume A3: for i being set st i in X holds
F . i is net of T ; :: thesis: F is net_set of X,T
let x be set ; :: according to YELLOW_6:def 12 :: thesis: ( x in rng F implies x is net of T )
assume x in rng F ; :: thesis: x is net of T
then ex i being set st
( i in dom F & x = F . i ) by FUNCT_1:def 3;
hence x is net of T by A3, A1; :: thesis: verum