let z be object ; for A, B, C, D being set st z in [:A,B,C,D:] holds
z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]
let A, B, C, D be set ; ( 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:]
; 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:51;
( not A is empty & not B is empty )
by A1, MCART_1:51;
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:10;
hence
z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]
; verum