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