hereby :: thesis: ( ( for n being Nat holds F . n is _Graph ) implies F is Graph-yielding )

assume A1: F is Graph-yielding ; :: thesis: for n being Nat holds F . n is _Graph
let n be Nat; :: thesis: F . n is _Graph
n in dom F by LmNat;
hence F . n is _Graph by A1; :: thesis: verum

end;

assume A2: for n being Nat holds F . n is _Graph ; :: thesis: F is Graph-yielding
let x be object ; :: according to GLIB_000:def 53 :: thesis: ( x in dom F implies F . x is _Graph )
assume x in dom F ; :: thesis: F . x is _Graph
hence F . x is _Graph by A2; :: thesis: verum