let p be ext-real number ; for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not p in rng (M . i) ) holds
for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)
let M be Matrix of ExtREAL; ( ( for i being Nat st i in dom M holds
not p in rng (M . i) ) implies for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j) )
assume A1:
for i being Nat st i in dom M holds
not p in rng (M . i)
; for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)
hereby verum
let j be
Nat;
( j in dom (M @) implies not p in rng ((M @) . j) )assume A2:
j in dom (M @)
;
not p in rng ((M @) . j)then A3:
(M @) . j = Line (
(M @),
j)
by MATRIX_0:60;
j in Seg (len (M @))
by A2, FINSEQ_1:def 3;
then
j in Seg (width M)
by MATRIX_0:def 6;
then A5:
Line (
(M @),
j)
= Col (
M,
j)
by MATRIX_0:59;
for
v being
object st
v in dom (Line ((M @),j)) holds
(Line ((M @),j)) . v <> p
proof
let v be
object ;
( v in dom (Line ((M @),j)) implies (Line ((M @),j)) . v <> p )
assume A6:
v in dom (Line ((M @),j))
;
(Line ((M @),j)) . v <> p
then reconsider i =
v as
Element of
NAT ;
( 1
<= i &
i <= len (Line ((M @),j)) )
by A6, FINSEQ_3:25;
then
( 1
<= i &
i <= width (M @) )
by MATRIX_0:def 7;
then
i in Seg (width (M @))
;
then
[j,i] in [:(dom (M @)),(Seg (width (M @))):]
by A2, ZFMISC_1:def 2;
then
[j,i] in Indices (M @)
by MATRIX_0:def 4;
then A7:
[i,j] in Indices M
by MATRIX_0:def 6;
then A8:
(
i in dom M &
j in dom (M . i) )
by MATRPROB:13;
then
(Line ((M @),j)) . v = M * (
i,
j)
by A5, MATRIX_0:def 8;
then
(Line ((M @),j)) . v = (M . i) . j
by A7, MATRPROB:14;
then
(Line ((M @),j)) . v in rng (M . i)
by A8, FUNCT_1:3;
hence
(Line ((M @),j)) . v <> p
by A1, A7, MATRPROB:13;
verum
end; hence
not
p in rng ((M @) . j)
by A3, FUNCT_1:def 3;
verum
end;