let n be Nat; for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular
let s1, s2 be FinSequence; ( len s1 = n & len s2 = n implies <*s1,s2*> is tabular )
assume A1:
( len s1 = n & len s2 = n )
; <*s1,s2*> is tabular
take
n
; MATRIX_0:def 1 for x being object st x in rng <*s1,s2*> holds
ex s being FinSequence st
( s = x & len s = n )
let x be object ; ( x in rng <*s1,s2*> implies ex s being FinSequence st
( s = x & len s = n ) )
assume
x in rng <*s1,s2*>
; ex s being FinSequence st
( s = x & len s = n )
then A2:
x in {s1,s2}
by FINSEQ_2:127;
then reconsider r = x as FinSequence by TARSKI:def 2;
take
r
; ( r = x & len r = n )
thus
( x = r & len r = n )
by A1, A2, TARSKI:def 2; verum