set I = the carrier of S;
set F0 = { the ZeroF of S};
set F1 = { the OneF of S};
set D1 = the carrier of S \ { the OneF of S};
set D0 = ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S};
set f = S TrivialArity ;
A1: dom (S TrivialArity) = the carrier of S \ { the OneF of S} by FUNCT_2:def 1;
for x being object st x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} holds
x in (S TrivialArity) " {0}

proof

let x be object ; :: thesis: ( x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} implies x in (S TrivialArity) " {0} )
assume A2: x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} ; :: thesis: x in (S TrivialArity) " {0}
then reconsider xx = x as Element of the carrier of S \ { the OneF of S} ;
not xx in { the ZeroF of S} by A2, XBOOLE_0:def 5;
then xx <> the ZeroF of S by TARSKI:def 1;
then ( TrivialArity xx = 0 & (S TrivialArity) . xx = TrivialArity xx ) by Def21, Def22;
then ( xx in dom (S TrivialArity) & (S TrivialArity) . xx in {0} ) by TARSKI:def 1, A1;
hence x in (S TrivialArity) " {0} by FUNCT_1:def 7; :: thesis: verum

end;

then A3: ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} c= (S TrivialArity) " {0} by TARSKI:def 3;
reconsider D11 = the carrier of S \ { the OneF of S} as infinite set ;
thus for b₁ being set st b₁ = (S TrivialArity) " {0} holds
not b₁ is finite by A3; :: thesis: verum