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) )
A1: rng pe c= rng (pe ^ qe) by FINSEQ_1:42;
rng qe c= rng (pe ^ qe) by FINSEQ_1:43;
hence ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) by A1, Th24; :: thesis: verum