let x, y, x1, y1, x9, y9, x19, y19 be object ; ( [[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]]
; ( 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; verum