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