let n, m be Nat; for D being non empty set
for f being FinSequence of D
for i, k being Nat
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let D be non empty set ; for f being FinSequence of D
for i, k being Nat
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let f be FinSequence of D; for i, k being Nat
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let i, k be Nat; for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let G be Matrix of D; ( rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G implies i <> k )
assume that
A1:
(rng f) /\ (rng (Col (G,i))) = {}
and
A2:
f /. n = G * (m,k)
and
A3:
n in dom f
and
A4:
m in dom G
and
A5:
i = k
; XBOOLE_0:def 7 contradiction
f . n = G * (m,k)
by A2, A3, PARTFUN1:def 6;
then A6:
G * (m,i) in rng f
by A3, A5, FUNCT_1:def 3;
A7:
( dom G = Seg (len G) & dom (Col (G,i)) = Seg (len (Col (G,i))) )
by FINSEQ_1:def 3;
( len (Col (G,i)) = len G & (Col (G,i)) . m = G * (m,i) )
by A4, Def8;
then
G * (m,i) in rng (Col (G,i))
by A4, A7, FUNCT_1:def 3;
hence
contradiction
by A1, A6, XBOOLE_0:def 4; verum