let D be non empty set ; :: thesis: for M being Matrix of D
for i being Element of NAT st i in Seg (width M) holds
rng (Col M,i) c= Values M
let M be Matrix of D; :: thesis: for i being Element of NAT st i in Seg (width M) holds
rng (Col M,i) c= Values M
let k be Element of NAT ; :: thesis: ( k in Seg (width M) implies rng (Col M,k) c= Values M )
assume A1: k in Seg (width M) ; :: thesis: rng (Col 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 (Col M,k) or e in Values M )
assume e in rng (Col M,k) ; :: thesis: e in Values M
then consider u being set such that
A3: u in dom (Col M,k) and
A4: e = (Col M,k) . u by FUNCT_1:def 5;
reconsider u = u as Element of NAT by A3;
A5: len (Col M,k) = len M by MATRIX_1:def 9;
then dom (Col M,k) = dom M by FINSEQ_3:31;
then A6: (Col M,k) . u = M * u,k by A3, MATRIX_1:def 9;
A7: ( 1 <= u & u <= len M ) by A3, A5, FINSEQ_3:27;
( 1 <= k & k <= width M ) by A1, FINSEQ_1:3;
then [u,k] in Indices M by A7, MATRIX_1:37;
hence e in Values M by A2, A4, A6; :: thesis: verum