let U be non empty set ; :: thesis: (peeler U) * ((id U) -class) = id U
set X = U;
set P = peeler U;
set IX = id U;
set I = (id U) -class ;
set IT = (peeler U) * ((id U) -class);
reconsider Pf = peeler U, If = (id U) -class as Function ;
A1: ( dom ((id U) -class) = U & dom (id U) = U ) by FUNCT_2:def 1;
A2: {_{U}_} = { {x} where x is Element of U : verum } by EQREL_1:37;
reconsider PP = peeler U as Function of (Class (id U)),U ;
reconsider II = (id U) -class as Function of U,(Class (id U)) ;
reconsider LH = PP * II, RH = id U as Function of U,U ;

now :: thesis: for x being Element of U holds (id U) . x = (PP * II) . x

let x be Element of U; :: thesis: (id U) . x = (PP * II) . x
set xx = x;
{x} in {_{U}_} by A2;
then reconsider xton = {x} as Element of {_{U}_} ;
(Pf * If) . x = Pf . (If . x) by A1, FUNCT_1:13
.= (peeler U) . (Class ((id U),x)) by Def13
.= (peeler U) . xton by EQREL_1:25
.= DeTrivial xton by Def12
.= x by Def11
.= (id U) . x ;
hence (id U) . x = (PP * II) . x ; :: thesis: verum

end;

hence (peeler U) * ((id U) -class) = id U by FUNCT_2:63; :: thesis: verum