deffunc H_{1}( 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_{1}(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

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

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