let z be object ; :: thesis: for A, B, C being set st z in [:A,B,C:] holds

( z `1_3 in A & z `2_3 in B & z `3_3 in C )

let A, B, C be set ; :: thesis: ( z in [:A,B,C:] implies ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) )

assume A1: z in [:A,B,C:] ; :: thesis: ( z `1_3 in A & z `2_3 in B & z `3_3 in C )

then A2: not C is empty by MCART_1:31;

A3: ( not A is empty & not B is empty ) by A1, MCART_1:31;

then consider a being Element of A, b being Element of B, c being Element of C such that

A4: z = [a,b,c] by A1, A2, DOMAIN_1:3;

A5: z `3_3 = c by A4;

( z `1_3 = a & z `2_3 = b ) by A4;

hence ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) by A3, A2, A5; :: thesis: verum

( z `1_3 in A & z `2_3 in B & z `3_3 in C )

let A, B, C be set ; :: thesis: ( z in [:A,B,C:] implies ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) )

assume A1: z in [:A,B,C:] ; :: thesis: ( z `1_3 in A & z `2_3 in B & z `3_3 in C )

then A2: not C is empty by MCART_1:31;

A3: ( not A is empty & not B is empty ) by A1, MCART_1:31;

then consider a being Element of A, b being Element of B, c being Element of C such that

A4: z = [a,b,c] by A1, A2, DOMAIN_1:3;

A5: z `3_3 = c by A4;

( z `1_3 = a & z `2_3 = b ) by A4;

hence ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) by A3, A2, A5; :: thesis: verum