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