deffunc H₁( Element of ) -> Element of Fin (DISJOINT_PAIRS A) = (@ u) \ (@ $1);
consider IT being Function of the carrier of (NormForm A), Fin (DISJOINT_PAIRS A) such that
A8: for v being Element of holds IT . v = H₁(v) from FUNCT_2:sch 4();

now

let v be Element of ; :: thesis: IT . v in the carrier of (NormForm A)
(@ u) \ (@ v) in Normal_forms_on A by Th8, XBOOLE_1:36;
then IT . v in Normal_forms_on A by A8;
hence IT . v in the carrier of (NormForm A) by NORMFORM:def 14; :: thesis: verum

end;

then reconsider IT = IT as UnOp of the carrier of (NormForm A) by Th1;
take IT ; :: thesis: for v being Element of holds IT . v = u \ v
let v be Element of ; :: thesis: IT . v = u \ v
v = @ v ;
hence IT . v = u \ v by A8; :: thesis: verum