let G be Graph; :: thesis: for pe, qe being FinSequence of the carrier' of G holds
( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) )
let pe, qe be FinSequence of the carrier' of G; :: thesis: ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) )
( rng pe c= rng (pe ^ qe) & rng qe c= rng (pe ^ qe) ) by FINSEQ_1:42, FINSEQ_1:43;
hence ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) by Th24; :: thesis: verum