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 k in dom M ; :: thesis: rng (Line M,k) c= Values M
then A1: ( 1 <= k & k <= len M ) by FINSEQ_3:27;
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
A2: u in dom (Line M,k) and
A3: e = (Line M,k) . u by FUNCT_1:def 5;
reconsider u = u as Element of NAT by A2;
A4: 1 <= u by A2, FINSEQ_3:27;
A5: len (Line M,k) = width M by MATRIX_1:def 8;
then u <= width M by A2, FINSEQ_3:27;
then A6: [k,u] in Indices M by A1, A4, MATRIX_1:37;
A7: Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } by GOBRD13:7;
dom (Line M,k) = Seg (width M) by A5, FINSEQ_1:def 3;
then (Line M,k) . u = M * k,u by A2, MATRIX_1:def 8;
hence e in Values M by A7, A3, A6; :: thesis: verum