let D be non empty set ; for M being Matrix of D
for i being Nat st i in dom M holds
rng (Line (M,i)) c= Values M
let M be Matrix of D; for i being Nat st i in dom M holds
rng (Line (M,i)) c= Values M
let k be Nat; ( k in dom M implies rng (Line (M,k)) c= Values M )
assume
k in dom M
; rng (Line (M,k)) c= Values M
then A1:
( 1 <= k & k <= len M )
by FINSEQ_3:25;
let e be object ; TARSKI:def 3 ( not e in rng (Line (M,k)) or e in Values M )
assume
e in rng (Line (M,k))
; e in Values M
then consider u being object such that
A2:
u in dom (Line (M,k))
and
A3:
e = (Line (M,k)) . u
by FUNCT_1:def 3;
reconsider u = u as Nat by A2;
A4:
1 <= u
by A2, FINSEQ_3:25;
A5:
len (Line (M,k)) = width M
by MATRIX_0:def 7;
then
u <= width M
by A2, FINSEQ_3:25;
then A6:
[k,u] in Indices M
by A1, A4, MATRIX_0:30;
A7:
Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
by MATRIX_0:39;
dom (Line (M,k)) = Seg (width M)
by A5, FINSEQ_1:def 3;
then
(Line (M,k)) . u = M * (k,u)
by A2, MATRIX_0:def 7;
hence
e in Values M
by A7, A3, A6; verum