set X = NAT ;
n const m is len-total
proof
let x, y be FinSequence of NAT ; :: according to COMPUT_1:def 2 :: thesis: ( len x = len y & x in dom (n const m) implies y in dom (n const m) )
assume that
A2: len x = len y and
A3: x in dom (n const m) ; :: thesis: y in dom (n const m)
len x = n by A3, CARD_1:def 7;
then y is Element of n -tuples_on NAT by A2, FINSEQ_2:92;
hence y in dom (n const m) ; :: thesis: verum
end;
hence ( n const m is len-total & not n const m is empty ) ; :: thesis: verum