let z, 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:35;
( not A is empty & not B is empty ) by A1, MCART_1:35;
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:15;
hence z = [(z `1_3),(z `2_3),(z `3_3)] by Th1; :: thesis: verum