let D be non empty set ; for k, n, m being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let k, n, m be Nat; for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let e1, e2 be FinSequence of D; ( len e1 = m & len e2 = m implies ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) ) )
assume A1:
( len e1 = m & len e2 = m )
; ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
consider e being FinSequence of D * such that
A2:
len e = n
and
A3:
for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) )
by Th9;
A4:
for i being Nat st i in dom e holds
len (e . i) = m
then reconsider e = e as Matrix of D by Th11;
for p being FinSequence of D st p in rng e holds
len p = m
then
e is Matrix of n,m,D
by A2, MATRIX_0:def 2;
hence
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
by A3; verum