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