let n, m be Nat; for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
let D be non empty set ; for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
let M be Matrix of n,m,D; for k being Nat st k in Seg n holds
M . k = Line (M,k)
let k be Nat; ( k in Seg n implies M . k = Line (M,k) )
assume A1:
k in Seg n
; M . k = Line (M,k)
( len M = n & dom M = Seg (len M) )
by Th25, FINSEQ_1:def 3;
then A2:
M . k in rng M
by A1, FUNCT_1:def 3;
per cases
( n = 0 or 0 < n )
;
suppose A3:
0 < n
;
M . k = Line (M,k)consider l being
Nat such that A4:
for
x being
object st
x in rng M holds
ex
p being
FinSequence of
D st
(
x = p &
len p = l )
by Th9;
consider p being
FinSequence of
D such that A5:
M . k = p
and
len p = l
by A2, A4;
A6:
width M = m
by A3, Th23;
A7:
for
j being
Nat st
j in Seg (width M) holds
p . j = M * (
k,
j)
proof
let j be
Nat;
( j in Seg (width M) implies p . j = M * (k,j) )
assume
j in Seg (width M)
;
p . j = M * (k,j)
then
[k,j] in [:(Seg n),(Seg m):]
by A1, A6, ZFMISC_1:87;
then
[k,j] in Indices M
by A3, Th23;
then
ex
q being
FinSequence of
D st
(
q = M . k &
M * (
k,
j)
= q . j )
by Def5;
hence
p . j = M * (
k,
j)
by A5;
verum
end;
len p = width M
by A2, A6, A5, Def2;
hence
M . k = Line (
M,
k)
by A5, A7, Def7;
verum end; end;