let F be Graph-yielding Function; :: thesis: ( F is Cycle-like implies F is connected )
assume A6: F is Cycle-like ; :: thesis: F is connected

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

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

end;

hence F is connected by GLIB_002:def 12; :: thesis: verum