reconsider M = F ^^ G as FinSequence ;
ex n being Nat st
for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )
proof
take n = () + (); :: thesis: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )

let x be object ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = n ) )

A1: ( rng F c= D * & rng G c= D * ) by FINSEQ_1:def 4;
assume x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n )

then consider y being object such that
A2: y in dom M and
A3: x = M . y by FUNCT_1:def 3;
A4: dom M = (dom F) /\ (dom G) by PRE_POLY:def 4;
then A5: y in dom G by ;
then A6: G . y in rng G by FUNCT_1:def 3;
A7: y in dom F by ;
then F . y in rng F by FUNCT_1:def 3;
then reconsider f = F . y, g = G . y as FinSequence of D by ;
reconsider y = y as Nat by ;
A8: G . y = Line (G,y) by ;
A9: x = f ^ g by ;
then reconsider p = x as FinSequence of D ;
take p ; :: thesis: ( x = p & len p = n )
thus x = p ; :: thesis: len p = n
F . y = Line (F,y) by ;
hence len p = (len (Line (F,y))) + (len (Line (G,y))) by
.= () + (len (Line (G,y))) by MATRIX_0:def 7
.= n by MATRIX_0:def 7 ;
:: thesis: verum
end;
hence F ^^ G is Matrix of D by MATRIX_0:9; :: thesis: verum