deffunc H₁( Element of , Element of ) -> 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 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 14;
take IT ; :: thesis: for u, v being Element of holds IT . u,v = mi ((@ u) =>> (@ v))
let u, v be Element of ; :: thesis: IT . u,v = mi ((@ u) =>> (@ v))
thus IT . u,v = mi ((@ u) =>> (@ v)) by A4; :: thesis: verum