let S be non degenerated ZeroOneStr ; :: thesis: (S TrivialArity) . the ZeroF of S = - 2
set f = S TrivialArity ;
set x0 = the ZeroF of S;
set x1 = the OneF of S;
( the ZeroF of S = 0. S & the OneF of S = 1. S & 0. S <> 1. S ) ;
then not the ZeroF of S in { the OneF of S} by TARSKI:def 1;
then reconsider x = the ZeroF of S as Element of the carrier of S \ { the OneF of S} by XBOOLE_0:def 5;
(S TrivialArity) . x = TrivialArity x by Def22
.= - 2 by Def21 ;
hence (S TrivialArity) . the ZeroF of S = - 2 ; :: thesis: verum