set C = MaxConstrSign ;
let n be Nat; :: according to ABCMIZ_A:def 12 :: thesis: for s being SortSymbol of MaxConstrSign holds not { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite
let s be SortSymbol of MaxConstrSign; :: thesis: not { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite
B1: the carrier of MaxConstrSign = {0,1,2} by ABCMIZ_1:def 9;
set X = { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } ;
consider l being quasi-loci such that
A0: len l = n by Th24;
deffunc H₁( set ) -> set = [s,[l,c₁]];
consider f being Function such that
A1: ( dom f = NAT & ( for i being set st i in NAT holds
f . i = H₁(i) ) ) from FUNCT_1:sch 3();
f is one-to-one

proof

let i, j be set ; :: according to FUNCT_1:def 8 :: thesis: ( not i in proj1 f or not j in proj1 f or not f . i = f . j or i = j )
assume ( i in dom f & j in dom f ) ; :: thesis: ( not f . i = f . j or i = j )
then reconsider i = i, j = j as Element of NAT by A1;
( f . i = H₁(i) & f . j = H₁(j) ) by A1;
then ( f . i = f . j implies [l,i] = [l,j] ) by ZFMISC_1:33;
hence ( not f . i = f . j or i = j ) by ZFMISC_1:33; :: thesis: verum

end;

then A2: not rng f is finite by A1, CARD_1:97;
rng f c= { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } )
assume y in rng f ; :: thesis: y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) }
then consider x being set such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A1, A3;
A4: ( [l,x] in [:QuasiLoci,NAT:] & y = H₁(x) ) by A1, A3;
then y in Constructors by B1, ThCs, ZFMISC_1:def 2;
then y in {*,non_op} \/ Constructors by XBOOLE_0:def 3;
then reconsider y = y as OperSymbol of MaxConstrSign by ABCMIZ_1:def 24;
A5: y is constructor by A4, ABCMIZ_1:def 11;
then A6: the_result_sort_of y = y `1 by ABCMIZ_1:def 24
.= s by A4, MCART_1:7 ;
len (the_arity_of y) = card ((y `2) `1) by A5, ABCMIZ_1:def 24
.= card ([l,x] `1) by A4, MCART_1:7
.= len l by MCART_1:7 ;
hence y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } by A0, A6; :: thesis: verum

end;

hence not { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite by A2; :: thesis: verum