set T = the Target of G;
set E = the carrier' of G;
set V = the carrier of G;
set Eit = the carrier' of G \/ {the carrier' of G};
set t = the carrier' of G .--> v2;
A1: {v1} c= the carrier of G by ZFMISC_1:37;
set Tit = the Target of G +* (the carrier' of G .--> v2);
A2: dom (the carrier' of G .--> v2) = {the carrier' of G} by FUNCOP_1:19;
A3: {v2} c= the carrier of G by ZFMISC_1:37;
( rng (the carrier' of G .--> v2) = {v2} & rng the Target of G c= the carrier of G ) by FUNCOP_1:14, RELAT_1:def 19;
then ( rng (the Target of G +* (the carrier' of G .--> v2)) c= (rng the Target of G) \/ (rng (the carrier' of G .--> v2)) & (rng the Target of G) \/ (rng (the carrier' of G .--> v2)) c= the carrier of G ) by A3, FUNCT_4:18, XBOOLE_1:8;
then A4: rng (the Target of G +* (the carrier' of G .--> v2)) c= the carrier of G by XBOOLE_1:1;
dom (the Target of G +* (the carrier' of G .--> v2)) = (dom the Target of G) \/ (dom (the carrier' of G .--> v2)) by FUNCT_4:def 1
.= the carrier' of G \/ {the carrier' of G} by A2, FUNCT_2:def 1 ;
then reconsider Tit = the Target of G +* (the carrier' of G .--> v2) as Function of (the carrier' of G \/ {the carrier' of G}),the carrier of G by A4, FUNCT_2:def 1, RELSET_1:11;
set S = the Source of G;
set s = the carrier' of G .--> v1;
A5: dom (the carrier' of G .--> v1) = {the carrier' of G} by FUNCOP_1:19;
set Sit = the Source of G +* (the carrier' of G .--> v1);
A6: dom (the Source of G +* (the carrier' of G .--> v1)) = (dom the Source of G) \/ (dom (the carrier' of G .--> v1)) by FUNCT_4:def 1
.= the carrier' of G \/ {the carrier' of G} by A5, FUNCT_2:def 1 ;
( rng (the carrier' of G .--> v1) = {v1} & rng the Source of G c= the carrier of G ) by FUNCOP_1:14, RELAT_1:def 19;
then ( rng (the Source of G +* (the carrier' of G .--> v1)) c= (rng the Source of G) \/ (rng (the carrier' of G .--> v1)) & (rng the Source of G) \/ (rng (the carrier' of G .--> v1)) c= the carrier of G ) by A1, FUNCT_4:18, XBOOLE_1:8;
then rng (the Source of G +* (the carrier' of G .--> v1)) c= the carrier of G by XBOOLE_1:1;
then reconsider Sit = the Source of G +* (the carrier' of G .--> v1) as Function of (the carrier' of G \/ {the carrier' of G}),the carrier of G by A6, FUNCT_2:def 1, RELSET_1:11;
reconsider IT = MultiGraphStruct(# the carrier of G,(the carrier' of G \/ {the carrier' of G}),Sit,Tit #) as non empty strict MultiGraphStruct ;
take IT ; :: thesis: ( the carrier of IT = the carrier of G & the carrier' of IT = the carrier' of G \/ {the carrier' of G} & the Source of IT = the Source of G +* (the carrier' of G .--> v1) & the Target of IT = the Target of G +* (the carrier' of G .--> v2) )
thus ( the carrier of IT = the carrier of G & the carrier' of IT = the carrier' of G \/ {the carrier' of G} & the Source of IT = the Source of G +* (the carrier' of G .--> v1) & the Target of IT = the Target of G +* (the carrier' of G .--> v2) ) ; :: thesis: verum