let D be non empty set ; for M being Matrix of D holds Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
let M be Matrix of D; Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
set V = { (M * (i,j)) where i, j is 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 Th35;
now for y being object holds
( ( y in Values M implies y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } ) & ( y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } implies y in Values M ) )let y be
object ;
( ( y in Values M implies y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } ) & ( y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } implies y in Values M ) )hereby ( y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } implies y in Values M )
assume
y in Values M
;
y in { (M * (i,j)) where i, j is 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 j being
Nat such that A6:
j in dom f
and A7:
f . j = y
by A2, A4, FINSEQ_2:10;
consider i being
Nat such that A8:
i in dom M
and A9:
M . i = f
by A5, FINSEQ_2:10;
reconsider i =
i,
j =
j as
Nat ;
A10:
[i,j] in Indices M
by A8, A9, A6, Th37;
then
ex
p being
FinSequence of
D st
(
p = M . i &
M * (
i,
j)
= p . j )
by Def5;
hence
y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
by A9, A7, A10;
verum
end; assume
y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
;
y in Values Mthen consider i,
j being
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, Def5;
j in dom f
by A12, A13, Th38;
then A15:
f . j in rng f
by FUNCT_1:def 3;
i in dom M
by A12, ZFMISC_1:87;
then A16:
M . i in rng M
by FUNCT_1:def 3;
f in D *
by FINSEQ_1:def 11;
then
rng f in { (rng f) where f is Element of D * : f in rng M }
by A13, A16;
hence
y in Values M
by A1, A11, A14, A15, TARSKI:def 4;
verum end;
hence
Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
by TARSKI:2; verum