let X1, X2, X3, X4, X5, X6 be set ; :: thesis: [:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4:],X5,X6:]
thus [:X1,X2,X3,X4,X5,X6:] = [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:] by MC39
.= [:[:[:[:X1,X2:],X3:],X4:],X5,X6:] by ZFMISC_1:def 3
.= [:[:X1,X2,X3,X4:],X5,X6:] by MCART_1:53 ; :: thesis: verum