let X, V be set ; :: thesis: for G being Graph
for pe, qe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds
(vertices qe) \ X c= V
let G be Graph; :: thesis: for pe, qe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds
(vertices qe) \ X c= V
let pe, qe be FinSequence of the carrier' of G; :: thesis: ( rng qe c= rng pe & (vertices pe) \ X c= V implies (vertices qe) \ X c= V )
assume that
A1: rng qe c= rng pe and
A2: (vertices pe) \ X c= V ; :: thesis: (vertices qe) \ X c= V
vertices qe c= vertices pe by A1, Th19;
then (vertices qe) \ X c= (vertices pe) \ X by XBOOLE_1:35;
hence (vertices qe) \ X c= V by A2; :: thesis: verum