let z be object ; :: thesis: for A, B, C, D being set st z in [:A,B,C,D:] holds
( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )
let A, B, C, D be set ; :: thesis: ( z in [:A,B,C,D:] implies ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D ) )
assume A1: z in [:A,B,C,D:] ; :: thesis: ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )
then A2: ( not C is empty & not D is empty ) by MCART_1:51;
A3: ( not A is empty & not B is empty ) by A1, MCART_1:51;
then consider a being Element of A, b being Element of B, c being Element of C, d being Element of D such that
A4: z = [a,b,c,d] by A1, A2, DOMAIN_1:10;
A5: ( z `3_4 = c & z `4_4 = d ) by A4;
( z `1_4 = a & z `2_4 = b ) by A4;
hence ( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D ) by A3, A2, A5; :: thesis: verum