deffunc H_{1}( Element of (NormForm A)) -> 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 (NormForm A) holds IT . v = H_{1}(v)
from FUNCT_2:sch 4();

take IT ; :: thesis: for v being Element of (NormForm A) holds IT . v = u \ v

let v be Element of (NormForm A); :: thesis: IT . v = u \ v

v = @ v ;

hence IT . v = u \ v by A8; :: thesis: verum

consider IT being Function of the carrier of (NormForm A),(Fin (DISJOINT_PAIRS A)) such that

A8: for v being Element of (NormForm A) holds IT . v = H

now :: thesis: for v being Element of (NormForm A) holds IT . v in the carrier of (NormForm A)

then reconsider IT = IT as UnOp of the carrier of (NormForm A) by Th1;let v be Element of (NormForm A); :: thesis: IT . v in the carrier of (NormForm A)

(@ u) \ (@ v) in Normal_forms_on A by Th4, 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 12; :: thesis: verum

end;(@ u) \ (@ v) in Normal_forms_on A by Th4, 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 12; :: thesis: verum

take IT ; :: thesis: for v being Element of (NormForm A) holds IT . v = u \ v

let v be Element of (NormForm A); :: thesis: IT . v = u \ v

v = @ v ;

hence IT . v = u \ v by A8; :: thesis: verum