hereby :: thesis: ( ( for x being Element of dom F holds F . x is Path-like ) implies F is Path-like )

assume A1: F is Path-like ; :: thesis: for x being Element of dom F holds F . x is Path-like
let x be Element of dom F; :: thesis: F . x is Path-like
consider G being _Graph such that
A2: ( F . x = G & G is Path-like ) by A1;
thus F . x is Path-like by A2; :: thesis: verum

end;

assume A3: for x being Element of dom F holds F . x is Path-like ; :: thesis: F is Path-like
let x be object ; :: according to GLPACY00:def 2 :: thesis: ( x in dom F implies ex G being _Graph st
( F . x = G & G is Path-like ) )
assume x in dom F ; :: thesis: ex G being _Graph st
( F . x = G & G is Path-like )
then reconsider y = x as Element of dom F ;
take F . y ; :: thesis: ( F . x = F . y & F . y is Path-like )
thus ( F . x = F . y & F . y is Path-like ) by A3; :: thesis: verum