reconsider M = F ^^ G as FinSequence ;
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);
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 ;
( 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
set such that A2:
y in dom M
and A3:
x = M . y
by FUNCT_1:def 5;
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 5;
A7:
y in dom F
by A2, A4, XBOOLE_0:def 4;
then
F . y in rng F
by FUNCT_1:def 5;
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:25;
A8:
G . y = Line G,
y
by A5, MATRIX_2:18;
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_2:18;
hence len p =
(len (Line F,y)) + (len (Line G,y))
by A9, A8, FINSEQ_1:35
.=
(width F) + (len (Line G,y))
by MATRIX_1:def 8
.=
n
by MATRIX_1:def 8
;
verum
end;
hence
F ^^ G is Matrix of D
by MATRIX_1:9; verum