let z, A, B, C, D, E be set ; :: thesis: ( z in [:A,B,C,D,E:] implies z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)] )
assume A1: z in [:A,B,C,D,E:] ; :: thesis: z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)]
then A2: ( not C is empty & not D is empty ) by MCART_2:11;
A3: not E is empty by A1, MCART_2:11;
( not A is empty & not B is empty ) by A1, MCART_2:11;
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 ex e being Element of E st z = [a,b,c,d,e] by A1, A2, A3, MCART_2:15;
hence z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)] by Th7; :: thesis: verum