deffunc H₁( Element of (NormForm A), Element of (NormForm A)) -> Element of Normal_forms_on A = mi ((@ $1) =>> (@ $2));
consider IT being Function of [: the carrier of (NormForm A), the carrier of (NormForm A):],(Normal_forms_on A) such that
A4: for u, v being Element of (NormForm A) holds IT . (u,v) = H₁(u,v) from BINOP_1:sch 4();
reconsider IT = IT as BinOp of the carrier of (NormForm A) by NORMFORM:def 12;
take IT ; :: thesis: for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v))
let u, v be Element of (NormForm A); :: thesis: IT . (u,v) = mi ((@ u) =>> (@ v))
thus IT . (u,v) = mi ((@ u) =>> (@ v)) by A4; :: thesis: verum