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();
the carrier of (NormForm A) = Normal_forms_on A by NORMFORM:def 14;
then reconsider IT = IT as UnOp of the carrier of (NormForm A) ;
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