let X1, X2, X3, X4, X5 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 x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
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 x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
let A2 be Subset of ; :: thesis: for A3 being Subset of
for A4 being Subset of
for A5 being Subset of
for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
let A3 be Subset of ; :: thesis: for A4 being Subset of
for A5 being Subset of
for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
let A4 be Subset of ; :: thesis: for A5 being Subset of
for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
let A5 be Subset of ; :: thesis: for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
let x be Element of [:X1,X2,X3,X4,X5:]; :: thesis: ( x in [:A1,A2,A3,A4,A5:] implies ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 ) )
assume A1: x in [:A1,A2,A3,A4,A5:] ; :: thesis: ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )
then reconsider y = x as Element of [:A1,A2,A3,A4,A5:] ;
A2 <> {} by A1, Th13;
then A2: y `2 in A2 ;
A4 <> {} by A1, Th13;
then A3: y `4 in A4 ;
A3 <> {} by A1, Th13;
then A4: y `3 in A3 ;
A5 <> {} by A1, Th13;
then A5: y `5 in A5 ;
A1 <> {} by A1, Th13;
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 ) by A2, A4, A3, A5, Th33; :: thesis: verum