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 )

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 A1: 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 A1, Def12; :: thesis: verum

end;

assume A2: 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 object st
( i in dom F & x = F . i ) by FUNCT_1:def 3;
hence x is net of T by A2; :: thesis: verum