let L be non empty RelStr ; :: thesis: for x being Element of L
for F being non empty NetStr over 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 over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
let F be non empty NetStr over 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: {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;
A2: RelStr(# the carrier of (x "/\" F), the InternalRel of (x "/\" F) #) = RelStr(# the carrier of F, the InternalRel of F #) by Def3;
then A3: dom the mapping of (x "/\" F) = the carrier of F by FUNCT_2:def 1;
A4: dom the mapping of F = the carrier of F by 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 object ; :: 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 object such that
A5: a in dom the mapping of (x "/\" F) and
A6: q = the mapping of (x "/\" F) . a by FUNCT_1:def 3;
reconsider a = a as Element of (x "/\" F) by A5;
consider y being Element of L such that
A7: y = the mapping of F . a and
A8: the mapping of (x "/\" F) . a = x "/\" y by Def3;
y in rng the mapping of F by A2, A4, A7, FUNCT_1:def 3;
hence q in {x} "/\" (rng the mapping of F) by A1, A6, A8; :: thesis: verum

end;

let q be object ; :: 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
A9: q = x "/\" y and
A10: y in rng the mapping of F by A1;
consider z being object such that
A11: z in dom the mapping of F and
A12: y = the mapping of F . z by A10, FUNCT_1:def 3;
reconsider z = z as Element of (x "/\" F) by A2, A11;
ex w being Element of L st
( w = the mapping of F . z & the mapping of (x "/\" F) . z = x "/\" w ) by Def3;
hence q in rng the mapping of (x "/\" F) by A3, A9, A11, A12, FUNCT_1:def 3; :: thesis: verum