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

z = [(z `1_3),(z `2_3),(z `3_3)]

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

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

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

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

then ex a being Element of A ex b being Element of B ex c being Element of C st z = [a,b,c] by A1, A2, DOMAIN_1:3;

hence z = [(z `1_3),(z `2_3),(z `3_3)] ; :: thesis: verum

z = [(z `1_3),(z `2_3),(z `3_3)]

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

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

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

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

then ex a being Element of A ex b being Element of B ex c being Element of C st z = [a,b,c] by A1, A2, DOMAIN_1:3;

hence z = [(z `1_3),(z `2_3),(z `3_3)] ; :: thesis: verum