let x1, x2, x3, x4 be object ; :: thesis: [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th38
.= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:29
.= {[[x1,x2],x3,x4]} by Th25
.= {[x1,x2,x3,x4]} ; :: thesis: verum