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 =
(width F) + (width G);
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 ;
( 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
;
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
;
( x = p & len p = n )
thus
x = p
;
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
;
verum
end;
hence
F ^^ G is Matrix of D
by MATRIX_0:9; verum