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