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 )]
( z `1_5 = a & z `2_5 = b & z `3_5 = c & z `4_5 = d & z `5_5 = e ) by A1, Def8, Def9, Def10, Def11, Def12;
hence z = [(z `1_5 ),(z `2_5 ),(z `3_5 ),(z `4_5 ),(z `5_5 )] by A1; :: thesis: verum