let G be Graph; :: thesis: for v1, v2 being Vertex of G holds
( the carrier' of G in the carrier' of (AddNewEdge v1,v2) & the carrier' of G = the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} & the Source of (AddNewEdge v1,v2) . the carrier' of G = v1 & the Target of (AddNewEdge v1,v2) . the carrier' of G = v2 )
let v1, v2 be Vertex of G; :: thesis: ( the carrier' of G in the carrier' of (AddNewEdge v1,v2) & the carrier' of G = the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} & the Source of (AddNewEdge v1,v2) . the carrier' of G = v1 & the Target of (AddNewEdge v1,v2) . the carrier' of G = v2 )
set G9 = AddNewEdge v1,v2;
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
set E9 = the carrier' of (AddNewEdge v1,v2);
A1: the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G} by Def7;
the carrier' of G in {the carrier' of G} by TARSKI:def 1;
hence the carrier' of G in the carrier' of (AddNewEdge v1,v2) by A1, XBOOLE_0:def 3; :: thesis: ( the carrier' of G = the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} & the Source of (AddNewEdge v1,v2) . the carrier' of G = v1 & the Target of (AddNewEdge v1,v2) . the carrier' of G = v2 )

now

let x be set ; :: thesis: ( ( x in the carrier' of G implies x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} ) & ( x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} implies x in the carrier' of G ) )

hereby :: thesis: ( x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} implies x in the carrier' of G )

assume A2: x in the carrier' of G ; :: thesis: x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G}
then x <> the carrier' of G ;
then A3: not x in {the carrier' of G} by TARSKI:def 1;
x in the carrier' of (AddNewEdge v1,v2) by A1, A2, XBOOLE_0:def 3;
hence x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: x in the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} ; :: thesis: x in the carrier' of G
then not x in {the carrier' of G} by XBOOLE_0:def 5;
hence x in the carrier' of G by A1, A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence the carrier' of G = the carrier' of (AddNewEdge v1,v2) \ {the carrier' of G} by TARSKI:2; :: thesis: ( the Source of (AddNewEdge v1,v2) . the carrier' of G = v1 & the Target of (AddNewEdge v1,v2) . the carrier' of G = v2 )
dom (the carrier' of G .--> v1) = {the carrier' of G} by FUNCOP_1:19;
then A5: the carrier' of G in dom (the carrier' of G .--> v1) by TARSKI:def 1;
the Source of (AddNewEdge v1,v2) = the Source of G +* (the carrier' of G .--> v1) by Def7;
hence the Source of (AddNewEdge v1,v2) . the carrier' of G = (the carrier' of G .--> v1) . the carrier' of G by A5, FUNCT_4:14
.= v1 by FUNCOP_1:87 ;
:: thesis: the Target of (AddNewEdge v1,v2) . the carrier' of G = v2
dom (the carrier' of G .--> v2) = {the carrier' of G} by FUNCOP_1:19;
then A6: the carrier' of G in dom (the carrier' of G .--> v2) by TARSKI:def 1;
the Target of (AddNewEdge v1,v2) = the Target of G +* (the carrier' of G .--> v2) by Def7;
hence the Target of (AddNewEdge v1,v2) . the carrier' of G = (the carrier' of G .--> v2) . the carrier' of G by A6, FUNCT_4:14
.= v2 by FUNCOP_1:87 ;
:: thesis: verum