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 ;

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

hence
(peeler U) * ((id U) -class) = id U
by FUNCT_2:63; :: thesis: verumlet 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;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