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

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

end;

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