let L be non empty RelStr ; :: thesis: for x being Element of L
for F being non empty NetStr of L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
let x be Element of L; :: thesis: for F being non empty NetStr of L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
let F be non empty NetStr of L; :: thesis: rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
set f = the mapping of F;
set h = the mapping of (x "/\" F);
set A = rng the mapping of F;
A1: RelStr(# the carrier of (x "/\" F),the InternalRel of (x "/\" F) #) = RelStr(# the carrier of F,the InternalRel of F #) by Def3;
A2: {x} "/\" (rng the mapping of F) = { (x "/\" y) where y is Element of L : y in rng the mapping of F } by YELLOW_4:42;
A3: dom the mapping of F = the carrier of F by FUNCT_2:def 1;
A4: dom the mapping of (x "/\" F) = the carrier of F by A1, FUNCT_2:def 1;
thus rng the mapping of (x "/\" F) c= {x} "/\" (rng the mapping of F) :: according to XBOOLE_0:def 10 :: thesis: {x} "/\" (rng the mapping of F) c= rng the mapping of (x "/\" F)

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in rng the mapping of (x "/\" F) or q in {x} "/\" (rng the mapping of F) )
assume q in rng the mapping of (x "/\" F) ; :: thesis: q in {x} "/\" (rng the mapping of F)
then consider a being set such that
A5: ( a in dom the mapping of (x "/\" F) & q = the mapping of (x "/\" F) . a ) by FUNCT_1:def 5;
reconsider a = a as Element of (x "/\" F) by A5;
consider y being Element of L such that
A6: ( y = the mapping of F . a & the mapping of (x "/\" F) . a = x "/\" y ) by Def3;
y in rng the mapping of F by A1, A3, A6, FUNCT_1:def 5;
hence q in {x} "/\" (rng the mapping of F) by A2, A5, A6; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} "/\" (rng the mapping of F) or q in rng the mapping of (x "/\" F) )
assume q in {x} "/\" (rng the mapping of F) ; :: thesis: q in rng the mapping of (x "/\" F)
then consider y being Element of L such that
A7: ( q = x "/\" y & y in rng the mapping of F ) by A2;
consider z being set such that
A8: ( z in dom the mapping of F & y = the mapping of F . z ) by A7, FUNCT_1:def 5;
reconsider z = z as Element of (x "/\" F) by A1, A8;
consider w being Element of L such that
A9: ( w = the mapping of F . z & the mapping of (x "/\" F) . z = x "/\" w ) by Def3;
thus q in rng the mapping of (x "/\" F) by A4, A7, A8, A9, FUNCT_1:def 5; :: thesis: verum