hereby :: thesis: ( ( for x being Element of dom GF holds GF . x is acyclic ) implies GF is acyclic )

assume A3:
for x being Element of dom GF holds GF . x is acyclic
; :: thesis: GF is acyclic assume A1:
GF is acyclic
; :: thesis: for x being Element of dom GF holds GF . x is acyclic

let x be Element of dom GF; :: thesis: GF . x is acyclic

consider G being _Graph such that

A2: ( GF . x = G & G is acyclic ) by A1;

thus GF . x is acyclic by A2; :: thesis: verum

end;let x be Element of dom GF; :: thesis: GF . x is acyclic

consider G being _Graph such that

A2: ( GF . x = G & G is acyclic ) by A1;

thus GF . x is acyclic by A2; :: thesis: verum

let x be object ; :: according to GLIB_002:def 13 :: thesis: ( x in dom GF implies ex G being _Graph st

( GF . x = G & G is acyclic ) )

assume x in dom GF ; :: thesis: ex G being _Graph st

( GF . x = G & G is acyclic )

then reconsider y = x as Element of dom GF ;

take GF . y ; :: thesis: ( GF . x = GF . y & GF . y is acyclic )

thus ( GF . x = GF . y & GF . y is acyclic ) by A3; :: thesis: verum