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)]
A2: z `3_4 = c by A1, Def6;
( z `1_4 = a & z `2_4 = b ) by A1, Def4, Def5;
hence z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)] by A1, A2, Def7; :: thesis: verum