take X ; :: thesis: ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X )
dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def 1;
hence ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) by RELAT_1:68; :: thesis: verum