let z be object ; for A, B, C being set st z in [:A,B,C:] holds
z = [(z `1_3),(z `2_3),(z `3_3)]
let A, B, C be set ; ( z in [:A,B,C:] implies z = [(z `1_3),(z `2_3),(z `3_3)] )
assume A1:
z in [:A,B,C:]
; z = [(z `1_3),(z `2_3),(z `3_3)]
then A2:
not C is empty
by MCART_1:31;
( not A is empty & not B is empty )
by A1, MCART_1:31;
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:3;
hence
z = [(z `1_3),(z `2_3),(z `3_3)]
; verum