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 )

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

hence
F ^^ G is Matrix of D
by MATRIX_0:9; :: thesis: verum
take n = (width F) + (width G); :: 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 A2, XBOOLE_0:def 4;

then A6: G . y in rng G by FUNCT_1:def 3;

A7: y in dom F by A2, A4, XBOOLE_0:def 4;

then F . y in rng F by FUNCT_1:def 3;

then reconsider f = F . y, g = G . y as FinSequence of D by A6, A1, FINSEQ_1:def 11;

reconsider y = y as Nat by A2, FINSEQ_3:23;

A8: G . y = Line (G,y) by A5, MATRIX_0:60;

A9: x = f ^ g by A2, A3, PRE_POLY:def 4;

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 A7, MATRIX_0:60;

hence len p = (len (Line (F,y))) + (len (Line (G,y))) by A9, A8, FINSEQ_1:22

.= (width F) + (len (Line (G,y))) by MATRIX_0:def 7

.= n by MATRIX_0:def 7 ;

:: thesis: verum

end;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 A2, XBOOLE_0:def 4;

then A6: G . y in rng G by FUNCT_1:def 3;

A7: y in dom F by A2, A4, XBOOLE_0:def 4;

then F . y in rng F by FUNCT_1:def 3;

then reconsider f = F . y, g = G . y as FinSequence of D by A6, A1, FINSEQ_1:def 11;

reconsider y = y as Nat by A2, FINSEQ_3:23;

A8: G . y = Line (G,y) by A5, MATRIX_0:60;

A9: x = f ^ g by A2, A3, PRE_POLY:def 4;

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 A7, MATRIX_0:60;

hence len p = (len (Line (F,y))) + (len (Line (G,y))) by A9, A8, FINSEQ_1:22

.= (width F) + (len (Line (G,y))) by MATRIX_0:def 7

.= n by MATRIX_0:def 7 ;

:: thesis: verum