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:
A2: ( 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 A3: for s being Element of the carrier of S \ { the OneF of S} holds IT1 . s = TrivialArity s ; :: thesis:
assume A4: for s being Element of the carrier of S \ { the OneF of S} holds IT2 . s = TrivialArity s ; :: thesis:

let x be object ; :: thesis:
assume x in dom IT1 ; :: thesis:
then reconsider s = x as Element of the carrier of S \ { the OneF of S} ;
IT1 . s = TrivialArity s by A3
.= IT2 . s by A4 ;
hence IT1 . x = IT2 . x ; :: thesis:

end;