let F be Graph-yielding Function; :: thesis: ( F is Path-like implies F is Tree-like )
assume A5: F is Path-like ; :: thesis: F is Tree-like

now :: thesis: for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & G is Tree-like )

let x be object ; :: thesis: ( x in dom F implies ex G being _Graph st
( G = F . x & G is Tree-like ) )
assume x in dom F ; :: thesis: ex G being _Graph st
( G = F . x & G is Tree-like )
then consider G being _Graph such that
A7: ( G = F . x & G is Path-like ) by A5;
take G = G; :: thesis: ( G = F . x & G is Tree-like )
thus ( G = F . x & G is Tree-like ) by A7; :: thesis: verum

end;

hence F is Tree-like by GLIB_002:def 14; :: thesis: verum