let i, n be Nat; for D being non empty set
for m being Nat
for f being FinSequence of D
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let D be non empty set ; for m being Nat
for f being FinSequence of D
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let m be Nat; for f being FinSequence of D
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let f be FinSequence of D; for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let G be Matrix of D; ( rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 implies f /. n in rng (Line ((DelCol (G,i)),m)) )
set D = DelCol (G,i);
assume that
A1:
rng f misses rng (Col (G,i))
and
A2:
f /. n in rng (Line (G,m))
and
A3:
n in dom f
and
A4:
i in Seg (width G)
and
A5:
m in dom G
and
A6:
width G > 1
; f /. n in rng (Line ((DelCol (G,i)),m))
A7:
( len (Line ((DelCol (G,i)),m)) = width (DelCol (G,i)) & dom (Line ((DelCol (G,i)),m)) = Seg (len (Line ((DelCol (G,i)),m))) )
by Def7, FINSEQ_1:def 3;
consider j being Nat such that
A8:
j in dom (Line (G,m))
and
A9:
f /. n = (Line (G,m)) . j
by A2, FINSEQ_2:10;
reconsider j = j as Nat ;
A10:
len (Line (G,m)) = width G
by Def7;
then A11:
j <= width G
by A8, FINSEQ_3:25;
A12:
dom (Line (G,m)) = Seg (len (Line (G,m)))
by FINSEQ_1:def 3;
then A13:
1 <= i
by A4, A10, FINSEQ_3:25;
A14:
f /. n = G * (m,j)
by A8, A9, A12, A10, Def7;
A15:
i <= width G
by A4, A12, A10, FINSEQ_3:25;
A16:
1 <= j
by A8, FINSEQ_3:25;
consider M being Nat such that
A17:
width G = M + 1
and
A18:
M > 0
by A6, SEQM_3:43;
A19:
width (DelCol (G,i)) = M
by A4, A17, Th63;
i <> j
by A1, A3, A5, A14, Th43;
per cases then
( j < i or i < j )
by XXREAL_0:1;
suppose A20:
j < i
;
f /. n in rng (Line ((DelCol (G,i)),m))then
j < width G
by A15, XXREAL_0:2;
then
j <= M
by A17, NAT_1:13;
then A21:
j in Seg (width (DelCol (G,i)))
by A16, A19, FINSEQ_1:1;
f /. n = (DelCol (G,i)) * (
m,
j)
by A4, A5, A14, A16, A17, A18, A20, Th69;
then
(Line ((DelCol (G,i)),m)) . j = f /. n
by A21, Def7;
hence
f /. n in rng (Line ((DelCol (G,i)),m))
by A7, A21, FUNCT_1:def 3;
verum end; suppose A22:
i < j
;
f /. n in rng (Line ((DelCol (G,i)),m))reconsider l =
j - 1 as
Element of
NAT by A16, INT_1:5;
A23:
l <= M
by A11, A17, XREAL_1:20;
i + 1
<= j
by A22, NAT_1:13;
then A24:
i <= l
by XREAL_1:19;
then
1
<= l
by A13, XXREAL_0:2;
then A25:
l in Seg (width (DelCol (G,i)))
by A19, A23, FINSEQ_1:1;
l + 1
= j
;
then
f /. n = (DelCol (G,i)) * (
m,
l)
by A4, A5, A14, A13, A17, A24, A23, Th70;
then
(Line ((DelCol (G,i)),m)) . l = f /. n
by A25, Def7;
hence
f /. n in rng (Line ((DelCol (G,i)),m))
by A7, A25, FUNCT_1:def 3;
verum end;