let k, l be Element of NAT ; :: thesis: <*[k,l]*> is FinSequence of [:NAT ,NAT :]
[k,l] in [:NAT ,NAT :] by ZFMISC_1:def 2;
then ( rng <*[k,l]*> = {[k,l]} & {[k,l]} c= [:NAT ,NAT :] ) by FINSEQ_1:56, ZFMISC_1:37;
hence <*[k,l]*> is FinSequence of [:NAT ,NAT :] by FINSEQ_1:def 4; :: thesis: verum