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:29, FINSEQ_1:30;
hence ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) by Th19; :: thesis: verum