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

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

proof

then
p ^^ q is FinSequence of (k + n) -tuples_on D
by FINSEQ_1:def 4;
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;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

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