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

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