let y, z be Element of X4; :: thesis: ( ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
y = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
z = x4 ) implies y = z )
assume A15: for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
y = x4 ; :: thesis: ( ex x1, x2, x3, x4, x5 being set st
( x = [x1,x2,x3,x4,x5] & not z = x4 ) or y = z )
assume A16: for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
z = x4 ; :: thesis: y = z
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4, xx5 being Element of X5 such that
A17: x = [xx1,xx2,xx3,xx4,xx5] by A1, Th17;
y = xx4 by A17, A15;
hence y = z by A17, A16; :: thesis: verum