consider x1, x2, x3, x4 being object such that
A1: x = [x1,x2,x3,x4] by Def9;
thus [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] = x by A1; :: thesis: verum