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 MC351
.= [:{[x1,x2]},{x3},{x4},{x5},{x6},{x7},{x8},{x9}:] by ZFMISC_1:35
.= {[[x1,x2],x3,x4,x5,x6,x7,x8,x9]} by Th27
.= {[x1,x2,x3,x4,x5,x6,x7,x8,x9]} by MC344 ; :: thesis: verum