let z1, z2 be set ; :: thesis: ( ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
z1 = y4 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
z2 = y4 ) implies z1 = z2 )
assume ( ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
z1 = y4 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
z2 = y4 ) ) ; :: thesis: z1 = z2
then ( z1 = x4 & z2 = x4 ) by A1;
hence z1 = z2 ; :: thesis: verum