let z be set ; :: thesis: ( ex a, b, c, d, e being set st z = [a,b,c,d,e] implies z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)] )
given a, b, c, d, e being set such that A1: z = [a,b,c,d,e] ; :: thesis: z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)]
A2: ( z `3_5 = c & z `4_5 = d ) by A1, Def10, Def11;
( z `1_5 = a & z `2_5 = b ) by A1, Def8, Def9;
hence z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)] by A1, A2, Def12; :: thesis: verum