let y5, X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ; :: thesis: for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y5 = xx5 ) holds
y5 = x `5
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]; :: thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y5 = xx5 ) implies y5 = x `5 )
assume that
A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) and
A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y5 = xx5 ; :: thesis: y5 = x `5
x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7),(x `8),(x `9)] by A1, Th182;
hence y5 = x `5 by A2; :: thesis: verum