set C = MaxConstrSign ;
let n be Nat; for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n
let s be SortSymbol of MaxConstrSign; ex m being constructor OperSymbol of s st len (the_arity_of m) = n
deffunc H1( Nat) -> object = [{},$1];
consider l being FinSequence such that
A1:
len l = n
and
A2:
for i being Nat st i in dom l holds
l . i = H1(i)
from FINSEQ_1:sch 2();
A3:
l is one-to-one
rng l c= Vars
then reconsider l = l as one-to-one FinSequence of Vars by A3, FINSEQ_1:def 4;
for i being Nat
for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j )
then reconsider l = l as quasi-loci by ABCMIZ_1:30;
set m = [s,[l,0]];
the carrier of MaxConstrSign = {a_Type,an_Adj,a_Term}
by ABCMIZ_1:def 9;
then A6:
[s,[l,0]] in Constructors
by Th28;
then
[s,[l,0]] in {*,non_op} \/ Constructors
by XBOOLE_0:def 3;
then reconsider m = [s,[l,0]] as constructor OperSymbol of MaxConstrSign by A6, Th42, ABCMIZ_1:def 24;
the_result_sort_of m =
m `1
by ABCMIZ_1:def 24
.=
s
;
then reconsider m = m as constructor OperSymbol of s by ABCMIZ_1:def 32;
take
m
; len (the_arity_of m) = n
thus len (the_arity_of m) =
card ((m `2) `1)
by ABCMIZ_1:def 24
.=
card ([l,0] `1)
.=
card l
.=
n
by A1
; verum