let y be object ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( ( 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) ) ) :: thesis: ( y in rng (/\\ (F,L)) iff ex x being object st

( x in dom F & y = //\ ((F . x),L) ) )

( x in dom F & y = //\ ((F . x),L) ) ) :: thesis: verum

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 ; :: thesis: 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; :: thesis: ( ( 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) ) ) :: thesis: ( y in rng (/\\ (F,L)) iff ex x being object st

( x in dom F & y = //\ ((F . x),L) ) )

proof

( 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 3; :: thesis: verum

end;

thus
( y in rng (/\\ (F,L)) iff ex x being object st hereby :: thesis: ( ex x being object st

( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) )

given x being object such that A2:
( x in dom F & y = \\/ ((F . x),L) )
; :: thesis: y in rng (\// (F,L))( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) )

assume
y in rng (\// (F,L))
; :: thesis: ex x being object st

( x in dom F & y = \\/ ((F . x),L) )

then consider x being object such that

A1: ( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by FUNCT_1:def 3;

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;( x in dom F & y = \\/ ((F . x),L) )

then consider x being object such that

A1: ( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by FUNCT_1:def 3;

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

( 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 3; :: thesis: verum

( x in dom F & y = //\ ((F . x),L) ) ) :: thesis: verum

proof

( 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 3; :: thesis: verum

end;

hereby :: thesis: ( ex x being object st

( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) )

given x being object such that A4:
( x in dom F & y = //\ ((F . x),L) )
; :: thesis: y in rng (/\\ (F,L))( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) )

assume
y in rng (/\\ (F,L))
; :: thesis: ex x being object st

( x in dom F & y = //\ ((F . x),L) )

then consider x being object such that

A3: ( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by FUNCT_1:def 3;

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;( x in dom F & y = //\ ((F . x),L) )

then consider x being object such that

A3: ( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by FUNCT_1:def 3;

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

( 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 3; :: thesis: verum