let F be Graph-yielding Function; :: thesis:
reconsider p = id (dom F) as one-to-one Function ;
take p ; :: thesis:
thus ( dom p = dom F & rng p = dom F ) ; :: thesis:
let x be object ; :: thesis:
assume A1: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G ; :: thesis:
take G ; :: thesis:
thus G = F . x ; :: thesis:
thus G = F . (p . x) by A1, FUNCT_1:18; :: thesis:
thus G is G -Disomorphic by GLIB_010:53; :: thesis: