let x be object ; :: thesis: for n, m being Nat holds m |-> (n |-> x) is tabular
let n, m be Nat; :: thesis: m |-> (n |-> x) is tabular
set s = m |-> (n |-> x);
reconsider n1 = n as Nat ;
take n1 ; :: according to MATRIX_0:def 1 :: thesis: for x being object st x in rng (m |-> (n |-> x)) holds
ex s being FinSequence st
( s = x & len s = n1 )
let z be object ; :: 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 )
take n |-> x ; :: thesis: ( n |-> x = z & len (n |-> x) = n1 )
rng (m |-> (n |-> x)) c= {(n |-> x)} by FUNCOP_1:13;
hence ( n |-> x = z & len (n |-> x) = n1 ) by A1, CARD_1:def 7, TARSKI:def 1; :: thesis: verum