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 A1: 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 )
thus ( 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 A1, FUNCT_2:7; :: thesis: verum