let IT1, IT2 be BinOp of the carrier of (SubstLatt V,C); :: thesis: ( ( for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
IT1 . u,v = mi (u9 =>> v9) ) & ( for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
IT2 . u,v = mi (u9 =>> v9) ) implies IT1 = IT2 )
assume that
A10: for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
IT1 . u,v = mi (u9 =>> v9) and
A11: for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
IT2 . u,v = mi (u9 =>> v9) ; :: thesis: IT1 = IT2

now

let u, v be Element of (SubstLatt V,C); :: thesis: IT1 . u,v = IT2 . u,v
reconsider u9 = u, v9 = v as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
thus IT1 . u,v = mi (u9 =>> v9) by A10
.= IT2 . u,v by A11 ; :: thesis: verum

end;

hence IT1 = IT2 by BINOP_1:2; :: thesis: verum