consider x1, x2, x3 being set such that
W: x = [x1,x2,x3] by Dfy;
( [x1,x2,x3] `1_3 = x1 & [x1,x2,x3] `2_3 = x2 & [x1,x2,x3] `3_3 = x3 ) ;
hence [(x `1_3),(x `2_3),(x `3_3)] = x by W; :: thesis: verum