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