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