let D be non empty set ; :: thesis: for M being Matrix of D holds Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
let M be Matrix of D; :: thesis: Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
set V = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } ;
set R = { (rng f) where f is Element of D * : f in rng M } ;
A1:
Values M = union { (rng f) where f is Element of D * : f in rng M }
by Th3;
now let y be
set ;
:: thesis: ( ( y in Values M implies y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } ) & ( y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } implies y in Values M ) )hereby :: thesis: ( y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } implies y in Values M )
assume
y in Values M
;
:: thesis: y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } then consider Y being
set such that A2:
y in Y
and A3:
Y in { (rng f) where f is Element of D * : f in rng M }
by A1, TARSKI:def 4;
consider f being
Element of
D * such that A4:
Y = rng f
and A5:
f in rng M
by A3;
consider i being
Nat such that A6:
i in dom M
and A7:
M . i = f
by A5, FINSEQ_2:11;
consider j being
Nat such that A8:
j in dom f
and A9:
f . j = y
by A2, A4, FINSEQ_2:11;
reconsider i =
i,
j =
j as
Element of
NAT by ORDINAL1:def 13;
A10:
[i,j] in Indices M
by A6, A7, A8, Th5;
then
ex
p being
FinSequence of
D st
(
p = M . i &
M * i,
j = p . j )
by MATRIX_1:def 6;
hence
y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
by A7, A9, A10;
:: thesis: verum
end; assume
y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
;
:: thesis: y in Values Mthen consider i,
j being
Element of
NAT such that A11:
y = M * i,
j
and A12:
[i,j] in Indices M
;
consider f being
FinSequence of
D such that A13:
f = M . i
and A14:
M * i,
j = f . j
by A12, MATRIX_1:def 6;
Indices M = [:(dom M),(Seg (width M)):]
by MATRIX_1:def 5;
then
i in dom M
by A12, ZFMISC_1:106;
then A15:
M . i in rng M
by FUNCT_1:def 5;
f in D *
by FINSEQ_1:def 11;
then A16:
rng f in { (rng f) where f is Element of D * : f in rng M }
by A13, A15;
j in dom f
by A12, A13, Th6;
then
f . j in rng f
by FUNCT_1:def 5;
hence
y in Values M
by A1, A11, A14, A16, TARSKI:def 4;
:: thesis: verum end;
hence
Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
by TARSKI:2; :: thesis: verum