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)

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

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 {x} "/\" (rng the mapping of F) or q in rng the mapping of (x "/\" F) )
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;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

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