let IT, IT' 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 IT' . v = u \ v ) implies IT = IT' )
assume that
A12: for v being Element of (SubstLatt V,C) holds IT . v = u \ v and
A13: for v being Element of (SubstLatt V,C) holds IT' . v = u \ v ; :: thesis: IT = IT'

now

let v be Element of (SubstLatt V,C); :: thesis: IT . v = IT' . v
thus IT . v = u \ v by A12
.= IT' . v by A13 ; :: thesis: verum

end;

hence IT = IT' by FUNCT_2:113; :: thesis: verum