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 & z `2 = y ) by A1, Def1, Def2;
hence [(z `1 ),(z `2 )] = z by A1; :: thesis: verum