let z, A, B, C, D be set ; :: thesis: ( z in [:A,B,C,D:] implies z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] )
assume A1: z in [:A,B,C,D:] ; :: thesis: z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]
then A2: ( not C is empty & not D is empty ) by MCART_1:55;
( not A is empty & not B is empty ) by A1, MCART_1:55;
then ex a being Element of A ex b being Element of B ex c being Element of C ex d being Element of D st z = [a,b,c,d] by A1, A2, DOMAIN_1:31;
hence z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] by Th4; :: thesis: verum