let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ; :: thesis: [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]
thus [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:[:[:[:[:[:X1,X2,X3:],X4:],X5:],X6:],X7:],X8:],X9:] by ZFMISC_1:def 4
.= [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:] by ZFMISC_1:def 3 ; :: thesis: verum