let e be Element of doms (n,k); :: thesis: e is Seg n -valued

per cases ( doms (n,k) is empty or not doms (n,k) is empty ) ;

suppose A1: doms (n,k) is empty ; :: thesis: e is Seg n -valued

e = {} by A1, SUBSET_1:def 1;
hence e is Seg n -valued by RELAT_1:171; :: thesis: verum

end;

suppose not doms (n,k) is empty ; :: thesis: e is Seg n -valued

then e in doms (n,k) ;
then ex s being Element of (Seg n) * st
( e = s & len s = k ) ;
hence e is Seg n -valued ; :: thesis: verum

end;

end;