let IT, IT9 be UnOp of the carrier of (SubstLatt (V,C)); :: thesis: ( ( for v being Element of (SubstLatt (V,C)) holds IT . v = u \ v ) & ( for v being Element of (SubstLatt (V,C)) holds IT9 . v = u \ v ) implies IT = IT9 )
assume that
A17: for v being Element of (SubstLatt (V,C)) holds IT . v = u \ v and
A18: for v being Element of (SubstLatt (V,C)) holds IT9 . v = u \ v ; :: thesis: IT = IT9

now :: thesis: for v being Element of (SubstLatt (V,C)) holds IT . v = IT9 . v

let v be Element of (SubstLatt (V,C)); :: thesis: IT . v = IT9 . v
thus IT . v = u \ v by A17
.= IT9 . v by A18 ; :: thesis: verum

end;

hence IT = IT9 by FUNCT_2:63; :: thesis: verum