deffunc H1( 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) = H1(u,v)
from BINOP_1:sch 4();
reconsider IT = IT as BinOp of the carrier of (NormForm A) by NORMFORM:def 12;
take
IT
; for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v))
let u, v be Element of (NormForm A); IT . (u,v) = mi ((@ u) =>> (@ v))
thus
IT . (u,v) = mi ((@ u) =>> (@ v))
by A4; verum