set C = MaxConstrSign ;
let n be Nat; :: according to ABCMIZ_A:def 12 :: thesis: for s being SortSymbol of MaxConstrSign holds { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite
let s be SortSymbol of MaxConstrSign; :: thesis: { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite
A1: 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
A2: len l = n by Th30;
deffunc H₁( object ) -> object = [s,[l,c₁]];
consider f being Function such that
A3: ( dom f = NAT & ( for i being object st i in NAT holds
f . i = H₁(i) ) ) from FUNCT_1:sch 3();
f is one-to-one

proof

let i, j be object ; :: according to FUNCT_1:def 4 :: 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 A3;
( f . i = H₁(i) & f . j = H₁(j) ) by A3;
then ( f . i = f . j implies [l,i] = [l,j] ) by XTUPLE_0:1;
hence ( not f . i = f . j or i = j ) by XTUPLE_0:1; :: thesis: verum

end;

then A4: rng f is infinite by A3, CARD_1:59;
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 object ; :: 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 object such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3, A5;
A6: ( [l,x] in [:QuasiLoci,NAT:] & y = H₁(x) ) by A3, A5;
then y in Constructors by A1, Th28, 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;
A7: y is constructor by A6;
then A8: the_result_sort_of y = y `1 by ABCMIZ_1:def 24
.= s by A6 ;
len (the_arity_of y) = card ((y `2) `1) by A7, ABCMIZ_1:def 24
.= card ([l,x] `1) by A6
.= len l ;
hence y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } by A2, A8; :: thesis: verum

end;

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