let n, k, m be Nat; :: thesis: (doms (k,n)) ^ (doms (k,m)) = doms (k,(n + m))
thus (doms (k,n)) ^ (doms (k,m)) c= doms (k,(n + m)) :: according to XBOOLE_0:def 10 :: thesis: doms (k,(n + m)) c= (doms (k,n)) ^ (doms (k,m))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (doms (k,n)) ^ (doms (k,m)) or y in doms (k,(n + m)) )
assume y in (doms (k,n)) ^ (doms (k,m)) ; :: thesis: y in doms (k,(n + m))
then ex p, s being FinSequence st
( y = p ^ s & p in doms (k,n) & s in doms (k,m) ) by POLNOT_1:def 2;
hence y in doms (k,(n + m)) by Th122; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in doms (k,(n + m)) or y in (doms (k,n)) ^ (doms (k,m)) )
assume A1: y in doms (k,(n + m)) ; :: thesis: y in (doms (k,n)) ^ (doms (k,m))
then consider p being Element of (Seg k) * such that
A2: ( p = y & len p = n + m ) ;
consider q being FinSequence such that
A3: p = (p | n) ^ q by FINSEQ_1:80;
len (p | n) = n by NAT_1:11, A2, FINSEQ_1:59;
then ( p | n in doms (k,n) & q in doms (k,m) ) by A1, A2, A3, Th120;
hence y in (doms (k,n)) ^ (doms (k,m)) by A2, A3, POLNOT_1:def 2; :: thesis: verum