let x, y, x1, y1, x9, y9, x19, y19 be object ; :: 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 XTUPLE_0:1;
hence ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) by XTUPLE_0:1; :: thesis: verum