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();
the carrier of (NormForm A) = Normal_forms_on A by NORMFORM:def 14;
then reconsider IT = IT as BinOp of the carrier of (NormForm A) ;
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