let z be set ; :: thesis: ( ex a, b, c being set st z = [a,b,c] implies z = [(z `1_3),(z `2_3),(z `3_3)] )
given a, b, c being set such that A1: z = [a,b,c] ; :: thesis: z = [(z `1_3),(z `2_3),(z `3_3)]
( z `1_3 = a & z `2_3 = b ) by A1, Def1, Def2;
hence z = [(z `1_3),(z `2_3),(z `3_3)] by A1, Def3; :: thesis: verum