deffunc H₁( Element of Quot. I) -> Element of Quot. I = qaddinv $1;
consider F being UnOp of (Quot. I) such that
A1: for u being Element of Quot. I holds F . u = H₁(u) from FUNCT_2:sch 4();
take F ; :: thesis: for u being Element of Quot. I holds F . u = qaddinv u
let u be Element of Quot. I; :: thesis: F . u = qaddinv u
thus F . u = qaddinv u by A1; :: thesis: verum