deffunc H₁( Element of AFV) -> Element of AFV = Pcom o,$1;
consider O being UnOp of the carrier of AFV such that
A1: for a being Element of AFV holds O . a = H₁(a) from FUNCT_2:sch 4();
take O ; :: thesis: for a being Element of AFV holds O . a = Pcom o,a
thus for a being Element of AFV holds O . a = Pcom o,a by A1; :: thesis: verum