let F be Graph-yielding Function; :: thesis: the_Source_of (rng F) = rng (the_Source_of F)
now :: thesis: for z being object holds
( ( z in the_Source_of (rng F) implies z in rng (the_Source_of F) ) & ( z in rng (the_Source_of F) implies z in the_Source_of (rng F) ) )
let z be object ; :: thesis: ( ( z in the_Source_of (rng F) implies z in rng (the_Source_of F) ) & ( z in rng (the_Source_of F) implies z in the_Source_of (rng F) ) )
hereby :: thesis: ( z in rng (the_Source_of F) implies z in the_Source_of (rng F) )
assume z in the_Source_of (rng F) ; :: thesis: z in rng (the_Source_of F)
then consider G1 being _Graph such that
A1: ( G1 in rng F & z = the_Source_of G1 ) by GLIB_014:def 16;
consider x being object such that
A2: ( x in dom F & G1 = F . x ) by A1, FUNCT_1:def 3;
consider G2 being _Graph such that
A3: ( G2 = F . x & (the_Source_of F) . x = the_Source_of G2 ) by A2, Def6;
x in dom (the_Source_of F) by A2, Def6;
hence z in rng (the_Source_of F) by A1, A2, A3, FUNCT_1:3; :: thesis: verum
end;
assume z in rng (the_Source_of F) ; :: thesis: z in the_Source_of (rng F)
then consider x being object such that
A4: ( x in dom (the_Source_of F) & z = (the_Source_of F) . x ) by FUNCT_1:def 3;
A5: x in dom F by A4, Def6;
then consider G1 being _Graph such that
A6: ( G1 = F . x & (the_Source_of F) . x = the_Source_of G1 ) by Def6;
G1 in rng F by A5, A6, FUNCT_1:3;
hence z in the_Source_of (rng F) by A4, A6, GLIB_014:def 16; :: thesis: verum
end;
hence the_Source_of (rng F) = rng (the_Source_of F) by TARSKI:2; :: thesis: verum