let e be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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)

proof

assume e in dom (the carrier' of G .--> v1) ; :: thesis: contradiction
then e in {the carrier' of G} by FUNCOP_1:19;
then e = the carrier' of G by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

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:12 ; :: thesis: the Target of (AddNewEdge v1,v2) . e = the Target of G . e
A3: not e in dom (the carrier' of G .--> v2)

proof

assume e in dom (the carrier' of G .--> v2) ; :: thesis: contradiction
then e in {the carrier' of G} by FUNCOP_1:19;
then e = the carrier' of G by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

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:12 ; :: thesis: verum