set V = the carrier of G;
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
set Eit = the carrier' of G \/ {the carrier' of G};
set s = the carrier' of G .--> v1;
set t = the carrier' of G .--> v2;
A1: ( dom (the carrier' of G .--> v1) = {the carrier' of G} & rng (the carrier' of G .--> v1) = {v1} ) by FUNCOP_1:14, FUNCOP_1:19;
set Sit = the Source of G +* (the carrier' of G .--> v1);
A2: 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 A1, FUNCT_2:def 1 ;
A3: rng the Source of G c= the carrier of G by RELAT_1:def 19;
A4: {v1} c= the carrier of G by ZFMISC_1:37;
A5: rng (the Source of G +* (the carrier' of G .--> v1)) c= (rng the Source of G) \/ (rng (the carrier' of G .--> v1)) by FUNCT_4:18;
(rng the Source of G) \/ (rng (the carrier' of G .--> v1)) c= the carrier of G by A1, A3, A4, XBOOLE_1:8;
then rng (the Source of G +* (the carrier' of G .--> v1)) c= the carrier of G by A5, 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 A2, FUNCT_2:def 1, RELSET_1:11;
A6: ( dom (the carrier' of G .--> v2) = {the carrier' of G} & rng (the carrier' of G .--> v2) = {v2} ) by FUNCOP_1:14, FUNCOP_1:19;
set Tit = the Target of G +* (the carrier' of G .--> v2);
A7: 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 A6, FUNCT_2:def 1 ;
A8: rng the Target of G c= the carrier of G by RELAT_1:def 19;
A9: {v2} c= the carrier of G by ZFMISC_1:37;
A10: rng (the Target of G +* (the carrier' of G .--> v2)) c= (rng the Target of G) \/ (rng (the carrier' of G .--> v2)) by FUNCT_4:18;
(rng the Target of G) \/ (rng (the carrier' of G .--> v2)) c= the carrier of G by A6, A8, A9, XBOOLE_1:8;
then rng (the Target of G +* (the carrier' of G .--> v2)) c= the carrier of G by A10, XBOOLE_1: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 A7, 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