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 :: thesis: for u, v being Element of (SubstLatt (V,C)) holds IT1 . (u,v) = IT2 . (u,v)

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