take x2 ; :: thesis: for y1, y2 being object st x = [y1,y2] holds
x2 = y2
thus for y1, y2 being object st x = [y1,y2] holds
x2 = y2 by A1, Th1; :: thesis: verum