let X, V be set ; :: thesis: for G being Graph
for qe, pe 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 qe, pe 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 qe, pe 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, Th24;
then (vertices qe) \ X c= (vertices pe) \ X by XBOOLE_1:35;
hence (vertices qe) \ X c= V by A2, XBOOLE_1:1; :: thesis: verum