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