let F, G be FinSequence-yielding FinSequence; :: thesis: (NAT -concatenation) .: [:(doms F),(doms G):] = doms (F ^ G)
set C = NAT -concatenation ;
thus (NAT -concatenation) .: [:(doms F),(doms G):] c= doms (F ^ G) :: according to XBOOLE_0:def 10 :: thesis: doms (F ^ G) c= (NAT -concatenation) .: [:(doms F),(doms G):]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (NAT -concatenation) .: [:(doms F),(doms G):] or y in doms (F ^ G) )
assume y in (NAT -concatenation) .: [:(doms F),(doms G):] ; :: thesis: y in doms (F ^ G)
then consider x being object such that
A1: ( x in dom (NAT -concatenation) & x in [:(doms F),(doms G):] & (NAT -concatenation) . x = y ) by FUNCT_1:def 6;
consider f, g being object such that
A2: ( f in doms F & g in doms G & x = [f,g] ) by A1, ZFMISC_1:def 2;
reconsider f = f, g = g as NAT -valued FinSequence by A2;
(NAT -concatenation) . (f,g) = f ^ g by FOMODEL0:4;
then y = f ^ g by A1, A2, BINOP_1:def 1;
hence y in doms (F ^ G) by A2, Th48; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in doms (F ^ G) or xy in (NAT -concatenation) .: [:(doms F),(doms G):] )
assume A3: xy in doms (F ^ G) ; :: thesis: xy in (NAT -concatenation) .: [:(doms F),(doms G):]
reconsider fg = xy as NAT -valued FinSequence by A3;
A4: ( len fg = len (F ^ G) & len (F ^ G) = (len F) + (len G) ) by A3, Th47, FINSEQ_1:22;
set f = fg | (len F);
A5: len (fg | (len F)) = len F by A4, NAT_1:11, FINSEQ_1:59;
consider g being FinSequence such that
A6: fg = (fg | (len F)) ^ g by FINSEQ_1:80;
A7: ( fg | (len F) in doms F & g in doms G ) by Th50, A3, A6, A5;
then A8: [(fg | (len F)),g] in [:(doms F),(doms G):] by ZFMISC_1:def 2;
( rng (fg | (len F)) c= NAT & rng g c= NAT ) by A7, RELAT_1:def 19;
then ( fg | (len F) is FinSequence of NAT & g is FinSequence of NAT ) by FINSEQ_1:def 4;
then ( fg | (len F) in NAT * & g in NAT * ) by FINSEQ_1:def 11;
then [(fg | (len F)),g] in [:(NAT *),(NAT *):] by ZFMISC_1:def 2;
then A9: [(fg | (len F)),g] in dom (NAT -concatenation) by FUNCT_2:def 1;
(NAT -concatenation) . ((fg | (len F)),g) = (fg | (len F)) ^ g by A7, FOMODEL0:4;
then (NAT -concatenation) . [(fg | (len F)),g] = (fg | (len F)) ^ g by BINOP_1:def 1;
hence xy in (NAT -concatenation) .: [:(doms F),(doms G):] by A6, A8, A9, FUNCT_1:def 6; :: thesis: verum