let z1, z2 be object ; :: thesis: ( ( for y1, y2 being object st x = [y1,y2] holds
z1 = y2 ) & ( for y1, y2 being object st x = [y1,y2] holds
z2 = y2 ) implies z1 = z2 )
assume that
A4: for y1, y2 being object st x = [y1,y2] holds
z1 = y2 and
A5: for y1, y2 being object st x = [y1,y2] holds
z2 = y2 ; :: thesis: z1 = z2
thus z1 = x2 by A1, A4
.= z2 by A1, A5 ; :: thesis: verum