let S be non empty standard-ins set ; :: thesis: for T being InsType of S ex I being Element of S st InsCode I = T
let T be InsType of S; :: thesis: ex I being Element of S st InsCode I = T
consider y being object such that
A1: [T,y] in proj1 S by XTUPLE_0:def 12;
consider z being object such that
A2: [[T,y],z] in S by A1, XTUPLE_0:def 12;
reconsider I = [[T,y],z] as Element of S by A2;
take I ; :: thesis: InsCode I = T
thus InsCode I = T ; :: thesis: verum