A1: rng (p ^' q) c= (rng p) \/ (rng q) by Th17;
A2: rng q c= D by FINSEQ_1:def 4;
rng p c= D by FINSEQ_1:def 4;
then (rng p) \/ (rng q) c= D by A2, XBOOLE_1:8;
then rng (p ^' q) c= D by A1;
hence p ^' q is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum