let z1, z2 be object ; :: thesis: ( ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
z1 = y3 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
z2 = y3 ) implies z1 = z2 )
assume that
A2: for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
z1 = y3 and
A3: for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
z2 = y3 ; :: thesis: z1 = z2
thus z1 = y3 by A2, A1
.= z2 by A1, A3 ; :: thesis: verum