let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L holds rng the mapping of N = { (N . i) where i is Element of N : verum }
let N be non empty NetStr over L; :: thesis: rng the mapping of N = { (N . i) where i is Element of N : verum }
set X = { (N . i) where i is Element of N : verum } ;
A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
thus rng the mapping of N c= { (N . i) where i is Element of N : verum } :: according to XBOOLE_0:def 10 :: thesis: { (N . i) where i is Element of N : verum } c= rng the mapping of N
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng the mapping of N or e in { (N . i) where i is Element of N : verum } )
assume e in rng the mapping of N ; :: thesis: e in { (N . i) where i is Element of N : verum }
then consider u being object such that
A2: u in dom the mapping of N and
A3: e = the mapping of N . u by FUNCT_1:def 3;
reconsider u = u as Element of N by A2;
e = N . u by A3;
hence e in { (N . i) where i is Element of N : verum } ; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (N . i) where i is Element of N : verum } or e in rng the mapping of N )
assume e in { (N . i) where i is Element of N : verum } ; :: thesis: e in rng the mapping of N
then ex i being Element of N st e = N . i ;
hence e in rng the mapping of N by A1, FUNCT_1:def 3; :: thesis: verum