let x1, x2, x3, x4 be set ; :: thesis: [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th54
.= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:35
.= {[[x1,x2],x3,x4]} by Th39
.= {[x1,x2,x3,x4]} ; :: thesis: verum