set V = union (the_Vertices_of S);
set E = union (the_Edges_of S);
reconsider s = union (the_Source_of S) as Function ;
( dom s = union (the_Edges_of S) & rng s c= union (the_Vertices_of S) ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider s = s as Function of (union (the_Edges_of S)),(union (the_Vertices_of S)) by FUNCT_2:2;
reconsider t = union (the_Target_of S) as Function ;
( dom t = union (the_Edges_of S) & rng t c= union (the_Vertices_of S) ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider t = t as Function of (union (the_Edges_of S)),(union (the_Vertices_of S)) by FUNCT_2:2;
take createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t) ; :: thesis: ( the_Vertices_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Vertices_of S) & the_Edges_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Edges_of S) & the_Source_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Source_of S) & the_Target_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Target_of S) )
thus ( the_Vertices_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Vertices_of S) & the_Edges_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Edges_of S) & the_Source_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Source_of S) & the_Target_of (createGraph ((union (the_Vertices_of S)),(union (the_Edges_of S)),s,t)) = union (the_Target_of S) ) ; :: thesis: verum