[:[:A,B,C:],D:] is finite ;
hence [:A,B,C,D:] is finite by ZFMISC_1:def 4; :: thesis: verum