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