deffunc H1( 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 = H1(v) from FUNCT_2:sch 4();
now :: thesis: for v being Element of (NormForm A) holds IT . v in the carrier of (NormForm A)
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;
then reconsider IT = IT as UnOp of the carrier of (NormForm A) by Th1;
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