rng (p ^^ q) c= (k + n) -tuples_on D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p ^^ q) or y in (k + n) -tuples_on D )
assume y in rng (p ^^ q) ; :: thesis: y in (k + n) -tuples_on D
then consider x being object such that
A1: x in dom (p ^^ q) and
A2: y = (p ^^ q) . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
A3: x in (dom p) /\ (dom q) by A1, PRE_POLY:def 4;
then A4: x in dom p by XBOOLE_0:def 4;
A5: x in dom q by A3, XBOOLE_0:def 4;
y = (p . x) ^ (q . x) by A1, A2, PRE_POLY:def 4
.= (p /. x) ^ (q . x) by A4, PARTFUN1:def 6
.= (p /. x) ^ (q /. x) by A5, PARTFUN1:def 6 ;
then y is Tuple of k + n,D ;
hence y in (k + n) -tuples_on D by FINSEQ_2:131; :: thesis: verum

end;

then p ^^ q is FinSequence of (k + n) -tuples_on D by FINSEQ_1:def 4;
hence p ^^ q is Element of ((k + n) -tuples_on D) * by FINSEQ_1:def 11; :: thesis: verum