let n, k, m be Nat; :: thesis: ( k <= n implies doms (k,m) c= doms (n,m) )
assume k <= n ; :: thesis: doms (k,m) c= doms (n,m)
then A1: Seg k c= Seg n by FINSEQ_1:5;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in doms (k,m) or y in doms (n,m) )
assume y in doms (k,m) ; :: thesis: y in doms (n,m)
then consider p being Element of (Seg k) * such that
A2: ( y = p & len p = m ) ;
rng p c= Seg n by A1;
then p is FinSequence of Seg n by FINSEQ_1:def 4;
then p in (Seg n) * by FINSEQ_1:def 11;
hence y in doms (n,m) by A2; :: thesis: verum