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) ) )
proof
hereby :: thesis: ( ex x being object 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 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;
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,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
( x in dom F & y = //\ ((F . x),L) ) ) :: thesis: verum
proof
hereby :: thesis: ( ex x being object 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 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;
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,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;