defpred S₁[ object , object ] means ex G being _Graph st
( G = F . $1 & $2 = the_Source_of G );
A17: for x, y1, y2 being object st x in dom F & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A18: for x being object st x in dom F holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom F implies ex y being object st S₁[x,y] )
assume x in dom F ; :: thesis: ex y being object st S₁[x,y]
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take the_Source_of G ; :: thesis: S₁[x, the_Source_of G]
take G ; :: thesis: ( G = F . x & the_Source_of G = the_Source_of G )
thus ( G = F . x & the_Source_of G = the_Source_of G ) ; :: thesis: verum

end;

consider f being Function such that
A19: ( dom f = dom F & ( for x being object st x in dom F holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A17, A18);
take f ; :: thesis: ( dom f = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Source_of G ) ) )
thus ( dom f = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Source_of G ) ) ) by A19; :: thesis: verum