deffunc H₁( Element of ) -> 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 holds IT . u = H₁(u) from FUNCT_2:sch 4();
reconsider IT = IT as UnOp of the carrier of (NormForm A) by NORMFORM:def 14;
take IT ; :: thesis: for u being Element of holds IT . u = mi (- (@ u))
let u be Element of ; :: thesis: IT . u = mi (- (@ u))
thus IT . u = mi (- (@ u)) by A1; :: thesis: verum