let x be set ; :: thesis: for m, n being Nat holds m |-> (n |-> x) is tabular
let m, n be Nat; :: thesis: m |-> (n |-> x) is tabular
set s = m |-> (n |-> x);
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
take n1 ; :: according to MATRIX_1:def 1 :: thesis: for x being set st x in rng (m |-> (n |-> x)) holds
ex s being FinSequence st
( s = x & len s = n1 )
let z be set ; :: thesis: ( z in rng (m |-> (n |-> x)) implies ex s being FinSequence st
( s = z & len s = n1 ) )
assume A1: z in rng (m |-> (n |-> x)) ; :: thesis: ex s being FinSequence st
( s = z & len s = n1 )
A2: rng (m |-> (n |-> x)) c= {(n |-> x)} by FUNCOP_1:19;
take t = n |-> x; :: thesis: ( t = z & len t = n1 )
thus ( t = z & len t = n1 ) by A1, A2, FINSEQ_1:def 18, TARSKI:def 1; :: thesis: verum