set D = the carrier of S \ { the OneF of S};
let IT1, IT2 be Function of ( the carrier of S \ { the OneF of S}),INT; :: thesis: ( ( for s being Element of the carrier of S \ { the OneF of S} holds IT1 . s = TrivialArity s ) & ( for s being Element of the carrier of S \ { the OneF of S} holds IT2 . s = TrivialArity s ) implies IT1 = IT2 )
Z0: ( dom IT1 = the carrier of S \ { the OneF of S} & dom IT2 = the carrier of S \ { the OneF of S} ) by FUNCT_2:def 1;
assume B1: for s being Element of the carrier of S \ { the OneF of S} holds IT1 . s = TrivialArity s ; :: thesis: ( ex s being Element of the carrier of S \ { the OneF of S} st not IT2 . s = TrivialArity s or IT1 = IT2 )
assume B2: for s being Element of the carrier of S \ { the OneF of S} holds IT2 . s = TrivialArity s ; :: thesis: IT1 = IT2

now

let x be set ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then reconsider s = x as Element of the carrier of S \ { the OneF of S} ;
IT1 . s = TrivialArity s by B1
.= IT2 . s by B2 ;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 by Z0, FUNCT_1:2; :: thesis: verum