let x, x9, y, y9, x1, x19, y1, y19 be set ; :: thesis: ( [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] implies ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) )
assume [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] ; :: thesis: ( x = x1 & y = y1 & x9 = x19 & y9 = y19 )
then ( [x,x9] = [x1,x19] & [y,y9] = [y1,y19] ) by ZFMISC_1:27;
hence ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) by ZFMISC_1:27; :: thesis: verum