let e be set ; for G being Graph
for v1, v2 being Vertex of G st e in the carrier' of G holds
( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )
let G be Graph; for v1, v2 being Vertex of G st e in the carrier' of G holds
( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )
let v1, v2 be Vertex of G; ( e in the carrier' of G implies ( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e ) )
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set G9 = AddNewEdge (v1,v2);
set S9 = the Source of (AddNewEdge (v1,v2));
set T9 = the Target of (AddNewEdge (v1,v2));
assume A1:
e in the carrier' of G
; ( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )
A2:
not e in dom ( the carrier' of G .--> v1)
thus the Source of (AddNewEdge (v1,v2)) . e =
( the Source of G +* ( the carrier' of G .--> v1)) . e
by Def7
.=
the Source of G . e
by A2, FUNCT_4:11
; the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e
A3:
not e in dom ( the carrier' of G .--> v2)
thus the Target of (AddNewEdge (v1,v2)) . e =
( the Target of G +* ( the carrier' of G .--> v2)) . e
by Def7
.=
the Target of G . e
by A3, FUNCT_4:11
; verum