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