let y be object ; for L being non empty RelStr
for F being Function-yielding Function holds
( ( y in rng (\// (F,L)) implies ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st
( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) )
let L be non empty RelStr ; for F being Function-yielding Function holds
( ( y in rng (\// (F,L)) implies ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st
( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) )
let F be Function-yielding Function; ( ( y in rng (\// (F,L)) implies ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st
( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) )
thus
( y in rng (\// (F,L)) iff ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) )
( y in rng (/\\ (F,L)) iff ex x being object st
( x in dom F & y = //\ ((F . x),L) ) )
thus
( y in rng (/\\ (F,L)) iff ex x being object st
( x in dom F & y = //\ ((F . x),L) ) )
verum