let z be set ; :: thesis: ( ex x, y being set st z = [x,y] implies [(z `1 ),(z `2 )] = z )
given x, y being set such that A1: z = [x,y] ; :: thesis: [(z `1 ),(z `2 )] = z
z `1 = x by A1, Def1;
hence [(z `1 ),(z `2 )] = z by A1, Def2; :: thesis: verum