let k, l be Element of NAT ; :: thesis: for e being Element of vSUB holds [<*[k,l]*>,e] in [:([:NAT,NAT:] *),vSUB:]
let e be Element of vSUB ; :: thesis: [<*[k,l]*>,e] in [:([:NAT,NAT:] *),vSUB:]
<*[k,l]*> in [:NAT,NAT:] * by FINSEQ_1:def 11;
hence [<*[k,l]*>,e] in [:([:NAT,NAT:] *),vSUB:] by ZFMISC_1:def 2; :: thesis: verum