take G ; :: thesis: ( the carrier of G c= the carrier of G & the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) )
thus the carrier of G c= the carrier of G ; :: thesis: ( the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) )
thus the carrier' of G c= the carrier' of G ; :: thesis: for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G )
let v be set ; :: thesis: ( v in the carrier' of G implies ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) )
assume v in the carrier' of G ; :: thesis: ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G )
hence ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5; :: thesis: verum