let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ; :: thesis: for A1 being Subset of
for A2 being Subset of
for A3 being Subset of
for A4 being Subset of
for A5 being Subset of
for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A1 be Subset of ; :: thesis: for A2 being Subset of
for A3 being Subset of
for A4 being Subset of
for A5 being Subset of
for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A2 be Subset of ; :: thesis: for A3 being Subset of
for A4 being Subset of
for A5 being Subset of
for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A3 be Subset of ; :: thesis: for A4 being Subset of
for A5 being Subset of
for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A4 be Subset of ; :: thesis: for A5 being Subset of
for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A5 be Subset of ; :: thesis: for A6 being Subset of
for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A6 be Subset of ; :: thesis: for A7 being Subset of
for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A7 be Subset of ; :: thesis: for A8 being Subset of
for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A8 be Subset of ; :: thesis: for A9 being Subset of
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let A9 be Subset of ; :: thesis: for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]; :: thesis: ( x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] implies ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 ) )
assume A1: x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] ; :: thesis: ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
then reconsider y = x as Element of [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] ;
A2 <> {} by A1, Th176;
then A2: y `2 in A2 ;
A8 <> {} by A1, Th176;
then A3: y `8 in A8 ;
A7 <> {} by A1, Th176;
then A4: y `7 in A7 ;
A6 <> {} by A1, Th176;
then A5: y `6 in A6 ;
A5 <> {} by A1, Th176;
then A6: y `5 in A5 ;
A9 <> {} by A1, Th176;
then A7: y `9 in A9 ;
A4 <> {} by A1, Th176;
then A8: y `4 in A4 ;
A3 <> {} by A1, Th176;
then A9: y `3 in A3 ;
A1 <> {} by A1, Th176;
then y `1 in A1 ;
hence ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 ) by A2, A9, A8, A6, A5, A4, A3, A7, Th199; :: thesis: verum