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