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
A18:
x = [xx1,xx2,xx3,xx4,xx5]
by A1, Th17;
take
xx5
; for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
xx5 = x5
thus
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
xx5 = x5
by A18, Th7; verum