let p be ext-real number ; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: for j being Nat st j in dom (M @) holds
not p in rng ((M @) . j)

hereby :: thesis: verum

let j be Nat; :: thesis: ( j in dom (M @) implies not p in rng ((M @) . j) )
assume A2: j in dom (M @) ; :: thesis: 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 ; :: thesis: ( v in dom (Line ((M @),j)) implies (Line ((M @),j)) . v <> p )
assume A6: v in dom (Line ((M @),j)) ; :: thesis: (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; :: thesis: verum

end;

hence not p in rng ((M @) . j) by A3, FUNCT_1:def 3; :: thesis: verum

end;