ex i being Element of NAT st dom (F ^^ G) = Seg i

proof

reconsider i = min (len F),(len G) as Element of NAT by FINSEQ_2:1;
take i ; :: thesis: dom (F ^^ G) = Seg i
thus dom (F ^^ G) = (dom F) /\ (dom G) by Def2
.= (dom F) /\ (Seg (len G)) by FINSEQ_1:def 3
.= (Seg (len F)) /\ (Seg (len G)) by FINSEQ_1:def 3
.= Seg i by FINSEQ_2:2 ; :: thesis: verum

end;

then reconsider M = F ^^ G as FinSequence by FINSEQ_1:def 2;
ex n being Nat st
for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )

proof

take n = (width F) + (width G); :: thesis: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )
let x be set ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = n ) )
assume x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n )
then consider y being set such that
A1: ( y in dom M & x = M . y ) by FUNCT_1:def 5;
dom M = (dom F) /\ (dom G) by Def2;
then A2: ( y in dom F & y in dom G ) by A1, XBOOLE_0:def 4;
then A3: ( F . y in rng F & G . y in rng G ) by FUNCT_1:def 5;
( rng F c= D * & rng G c= D * ) by FINSEQ_1:def 4;
then reconsider f = F . y, g = G . y as FinSequence of D by A3, FINSEQ_1:def 11;
A4: x = f ^ g by A1, Def2;
then reconsider p = x as FinSequence of D ;
take p ; :: thesis: ( x = p & len p = n )
thus x = p ; :: thesis: len p = n
reconsider y = y as Nat by A1, FINSEQ_3:25;
( F . y = Line F,y & G . y = Line G,y ) by A2, MATRIX_2:18;
hence len p = (len (Line F,y)) + (len (Line G,y)) by A4, FINSEQ_1:35
.= (width F) + (len (Line G,y)) by MATRIX_1:def 8
.= n by MATRIX_1:def 8 ;
:: thesis: verum

end;

hence F ^^ G is Matrix of D by MATRIX_1:9; :: thesis: verum