let z be set ; :: thesis: ( ex a, b, c, d being set st z = [a,b,c,d] implies z = [(z `1_4 ),(z `2_4 ),(z `3_4 ),(z `4_4 )] )
given a, b, c, d being set such that A1: z = [a,b,c,d] ; :: thesis: z = [(z `1_4 ),(z `2_4 ),(z `3_4 ),(z `4_4 )]
( z `1_4 = a & z `2_4 = b & z `3_4 = c & z `4_4 = d ) by A1, Def4, Def5, Def6, Def7;
hence z = [(z `1_4 ),(z `2_4 ),(z `3_4 ),(z `4_4 )] by A1; :: thesis: verum