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 k in Seg (width M) ; :: thesis: rng (Col M,k) c= Values M
then A1: ( 1 <= k & k <= width M ) by FINSEQ_1:3;
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
A2: u in dom (Col M,k) and
A3: e = (Col 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 (Col M,k) = len M by MATRIX_1:def 9;
then u <= len M by A2, FINSEQ_3:27;
then A6: [u,k] in Indices M by A4, A1, 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 (Col M,k) = dom M by A5, FINSEQ_3:31;
then (Col M,k) . u = M * u,k by A2, MATRIX_1:def 9;
hence e in Values M by A7, A3, A6; :: thesis: verum