let x1, x2, x3, x4, x5 be set ; :: thesis: [:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}
thus [:{x1},{x2},{x3},{x4},{x5}:] = [:[:{x1},{x2}:],{x3},{x4},{x5}:] by Th12
.= [:{[x1,x2]},{x3},{x4},{x5}:] by ZFMISC_1:29
.= {[[x1,x2],x3,x4,x5]} by MCART_1:61
.= {[x1,x2,x3,x4,x5]} by Th6 ; :: thesis: verum