let n, m be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to XBOOLE_0:def 7 :: thesis: 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; :: thesis: verum