reconsider S = (V * (the_Source_of G)) * (E ") as Function of (rng E),(rng V) by Lm1;
reconsider T = (V * (the_Target_of G)) * (E ") as Function of (rng E),(rng V) by Lm1;
take createGraph ((rng V),(rng E),S,T) ; :: thesis: ex S, T being Function of (rng E),(rng V) st
( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & createGraph ((rng V),(rng E),S,T) = createGraph ((rng V),(rng E),S,T) )
take S ; :: thesis: ex T being Function of (rng E),(rng V) st
( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & createGraph ((rng V),(rng E),S,T) = createGraph ((rng V),(rng E),S,T) )
take T ; :: thesis: ( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & createGraph ((rng V),(rng E),S,T) = createGraph ((rng V),(rng E),S,T) )
thus ( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & createGraph ((rng V),(rng E),S,T) = createGraph ((rng V),(rng E),S,T) ) ; :: thesis: verum