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

now

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

end;

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