let V be non empty set ; :: thesis: for E being set
for S, T being Function of E,V st ( for v being Element of V holds
( S " {v} is finite & T " {v} is finite ) ) holds
createGraph (V,E,S,T) is locally-finite
let E be set ; :: thesis: for S, T being Function of E,V st ( for v being Element of V holds
( S " {v} is finite & T " {v} is finite ) ) holds
createGraph (V,E,S,T) is locally-finite
let S, T be Function of E,V; :: thesis: ( ( for v being Element of V holds
( S " {v} is finite & T " {v} is finite ) ) implies createGraph (V,E,S,T) is locally-finite )
assume A1: for v being Element of V holds
( S " {v} is finite & T " {v} is finite ) ; :: thesis: createGraph (V,E,S,T) is locally-finite
set G = createGraph (V,E,S,T);
now :: thesis: for v being Vertex of (createGraph (V,E,S,T)) holds
( v .edgesIn() is finite & v .edgesOut() is finite )
let v be Vertex of (createGraph (V,E,S,T)); :: thesis: ( v .edgesIn() is finite & v .edgesOut() is finite )
( S " {v} is finite & T " {v} is finite ) by A1;
then ( (the_Source_of (createGraph (V,E,S,T))) " {v} is finite & (the_Target_of (createGraph (V,E,S,T))) " {v} is finite ) ;
hence ( v .edgesIn() is finite & v .edgesOut() is finite ) by GLIBPRE0:25; :: thesis: verum
end;
hence createGraph (V,E,S,T) is locally-finite by Th25; :: thesis: verum