let y be set ; :: thesis: for L being non empty RelStr
for F being Function-yielding Function holds
( ( y in rng (\// F,L) implies ex x being set st
( x in dom F & y = \\/ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) ) & ( y in rng (/\\ F,L) implies ex x being set st
( x in dom F & y = //\ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = //\ (F . x),L ) implies y in rng (/\\ F,L) ) )
let L be non empty RelStr ; :: thesis: for F being Function-yielding Function holds
( ( y in rng (\// F,L) implies ex x being set st
( x in dom F & y = \\/ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) ) & ( y in rng (/\\ F,L) implies ex x being set st
( x in dom F & y = //\ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = //\ (F . x),L ) implies y in rng (/\\ F,L) ) )
let F be Function-yielding Function; :: thesis: ( ( y in rng (\// F,L) implies ex x being set st
( x in dom F & y = \\/ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) ) & ( y in rng (/\\ F,L) implies ex x being set st
( x in dom F & y = //\ (F . x),L ) ) & ( ex x being set 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 set st
( x in dom F & y = \\/ (F . x),L ) ) :: thesis: ( y in rng (/\\ F,L) iff ex x being set st
( x in dom F & y = //\ (F . x),L ) )

proof

hereby :: thesis: ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) )

assume y in rng (\// F,L) ; :: thesis: ex x being set st
( x in dom F & y = \\/ (F . x),L )
then consider x being set such that
A1: ( x in dom (\// F,L) & y = (\// F,L) . x ) by FUNCT_1:def 5;
take x = x; :: thesis: ( x in dom F & y = \\/ (F . x),L )
thus ( x in dom F & y = \\/ (F . x),L ) by A1, Def1; :: thesis: verum

end;

given x being set such that A2: ( x in dom F & y = \\/ (F . x),L ) ; :: thesis: y in rng (\// F,L)
( x in dom (\// F,L) & y = (\// F,L) . x ) by A2, Def1, FUNCT_2:def 1;
hence y in rng (\// F,L) by FUNCT_1:def 5; :: thesis: verum

end;

thus ( y in rng (/\\ F,L) iff ex x being set st
( x in dom F & y = //\ (F . x),L ) ) :: thesis: verum

proof

hereby :: thesis: ( ex x being set st
( x in dom F & y = //\ (F . x),L ) implies y in rng (/\\ F,L) )

assume y in rng (/\\ F,L) ; :: thesis: ex x being set st
( x in dom F & y = //\ (F . x),L )
then consider x being set such that
A3: ( x in dom (/\\ F,L) & y = (/\\ F,L) . x ) by FUNCT_1:def 5;
take x = x; :: thesis: ( x in dom F & y = //\ (F . x),L )
thus ( x in dom F & y = //\ (F . x),L ) by A3, Def2; :: thesis: verum

end;

given x being set such that A4: ( x in dom F & y = //\ (F . x),L ) ; :: thesis: y in rng (/\\ F,L)
( x in dom (/\\ F,L) & y = (/\\ F,L) . x ) by A4, Def2, FUNCT_2:def 1;
hence y in rng (/\\ F,L) by FUNCT_1:def 5; :: thesis: verum

end;