let G be _Graph; :: thesis: for x being set
for n being Nat st not n in _GraphSelectors holds
( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph )
let x be set ; :: thesis: for n being Nat st not n in _GraphSelectors holds
( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph )
let n be Nat; :: thesis: ( not n in _GraphSelectors implies ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) )
set G2 = G .set (n,x);
A1: dom G c= dom (G .set (n,x)) by FUNCT_4:10;
assume A2: not n in _GraphSelectors ; :: thesis: ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph )
then EdgeSelector <> n by ENUMSET1:def 2;
then A3: not EdgeSelector in dom (n .--> x) by TARSKI:def 1;
TargetSelector <> n by A2, ENUMSET1:def 2;
then A4: not TargetSelector in dom (n .--> x) by TARSKI:def 1;
SourceSelector <> n by A2, ENUMSET1:def 2;
then A5: not SourceSelector in dom (n .--> x) by TARSKI:def 1;
VertexSelector <> n by A2, ENUMSET1:def 2;
then not VertexSelector in dom (n .--> x) by TARSKI:def 1;
hence A6: ( the_Vertices_of (G .set (n,x)) = the_Vertices_of G & the_Edges_of (G .set (n,x)) = the_Edges_of G & the_Source_of (G .set (n,x)) = the_Source_of G & the_Target_of (G .set (n,x)) = the_Target_of G ) by A3, A5, A4, FUNCT_4:11; :: thesis: G .set (n,x) is _Graph
A7: ( SourceSelector in dom G & TargetSelector in dom G ) by Def10;
( VertexSelector in dom G & EdgeSelector in dom G ) by Def10;
hence G .set (n,x) is _Graph by A7, A1, A6, Def10; :: thesis: verum