deffunc H₁( Element of (NormForm A)) -> Element of Normal_forms_on A = mi (- (@ $1));
consider IT being Function of the carrier of (NormForm A),(Normal_forms_on A) such that
A1: for u being Element of (NormForm A) holds IT . u = H₁(u) from FUNCT_2:sch 4();
reconsider IT = IT as UnOp of the carrier of (NormForm A) by NORMFORM:def 12;
take IT ; :: thesis: for u being Element of (NormForm A) holds IT . u = mi (- (@ u))
let u be Element of (NormForm A); :: thesis: IT . u = mi (- (@ u))
thus IT . u = mi (- (@ u)) by A1; :: thesis: verum