let L be non empty RelStr ; 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; 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; 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)
XBOOLE_0:def 10 {x} "/\" (rng the mapping of F) c= rng the mapping of (x "/\" F)
let q be object ; TARSKI:def 3 ( 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)
; 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; verum