let x, x', y, y', x1, x1', y1, y1' be set ; :: thesis: ( [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] implies ( x = x1 & y = y1 & x' = x1' & y' = y1' ) )
assume [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] ; :: thesis: ( x = x1 & y = y1 & x' = x1' & y' = y1' )
then ( [x,x'] = [x1,x1'] & [y,y'] = [y1,y1'] ) by ZFMISC_1:33;
hence ( x = x1 & y = y1 & x' = x1' & y' = y1' ) by ZFMISC_1:33; :: thesis: verum