consider x1, x2 being set such that
W: x = [x1,x2] by Dfx;
thus [(x `1),(x `2)] = [x1,(x `2)] by W, Def1
.= x by W, Def2 ; :: thesis: verum