thus ( F is Graph-yielding implies for n being Nat holds F . n is _Graph ) by LmNat; :: thesis: ( ( for n being Nat holds F . n is _Graph ) implies F is Graph-yielding )
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