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:39, ZFMISC_1:31;
hence <*[k,l]*> is FinSequence of [:NAT,NAT:] by FINSEQ_1:def 4; :: thesis: verum