let i, n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A22: i < j ; :: thesis: 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; :: thesis: verum

end;

end;