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:31;
set Tit = the Target of G +* ( the carrier' of G .--> v2);
A3: {v2} c= the carrier of G by ZFMISC_1:31;
( rng ( the carrier' of G .--> v2) = {v2} & rng the Target of G c= the carrier of G ) by FUNCOP_1:8, 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:17, XBOOLE_1:8;
then A4: rng ( the Target of G +* ( the carrier' of G .--> v2)) c= the carrier of G ;
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 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:4;
set S = the Source of G;
set s = the carrier' of G .--> v1;
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 FUNCT_2:def 1 ;
( rng ( the carrier' of G .--> v1) = {v1} & rng the Source of G c= the carrier of G ) by FUNCOP_1:8, 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:17, XBOOLE_1:8;
then rng ( the Source of G +* ( the carrier' of G .--> v1)) c= the carrier of G ;
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:4;
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