let F be Graph-yielding Function; :: thesis: ( F is vertex-disjoint implies F is one-to-one )
assume A1: F is vertex-disjoint ; :: thesis: F is one-to-one
now :: thesis: for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
not x1 <> x2
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies not x1 <> x2 )
assume A2: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: not x1 <> x2
assume x1 <> x2 ; :: thesis: contradiction
then consider G1, G2 being _Graph such that
A3: ( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_of G2 ) by A1, A2;
thus contradiction by A2, A3; :: thesis: verum
end;
hence F is one-to-one by FUNCT_1:def 4; :: thesis: verum