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