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