let n be Nat; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: <*s1,s2,s3*> is tabular

now :: thesis: 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; :: thesis: 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 ; :: thesis: ( x in rng <*s1,s2,s3*> implies ex r being FinSequence st
( x = r & len r = n ) )
assume x in rng <*s1,s2,s3*> ; :: thesis: 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; :: thesis: ( x = r & len r = n )
thus ( x = r & len r = n ) by A1, A2, ENUMSET1:def 1; :: thesis: verum

end;

hence <*s1,s2,s3*> is tabular ; :: thesis: verum