let z, A, B, C, D, E be set ; :: thesis: ( z in [:A,B,C,D,E:] implies ( z `1_5 in A & z `2_5 in B & z `3_5 in C & z `4_5 in D & z `5_5 in E ) )
assume A1: z in [:A,B,C,D,E:] ; :: thesis: ( z `1_5 in A & z `2_5 in B & z `3_5 in C & z `4_5 in D & z `5_5 in E )
then A2: ( not C is empty & not D is empty ) by MCART_2:11;
A3: not E is empty by A1, MCART_2:11;
A4: ( not A is empty & not B is empty ) by A1, MCART_2:11;
then consider a being Element of A, b being Element of B, c being Element of C, d being Element of D, e being Element of E such that
A5: z = [a,b,c,d,e] by A1, A2, A3, MCART_2:15;
A6: z `5_5 = e by A5, Def12;
A7: ( z `3_5 = c & z `4_5 = d ) by A5, Def10, Def11;
( z `1_5 = a & z `2_5 = b ) by A5, Def8, Def9;
hence ( z `1_5 in A & z `2_5 in B & z `3_5 in C & z `4_5 in D & z `5_5 in E ) by A4, A2, A3, A7, A6; :: thesis: verum