set C = MaxConstrSign ;
let n be Nat; :: thesis: 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 ; :: thesis: ex m being constructor OperSymbol of s st len (the_arity_of m) = n
deffunc H₁( Nat) -> set = [{} ,$1];
consider l being FinSequence such that
F0: len l = n and
F1: for i being Nat st i in dom l holds
l . i = H₁(i) from FINSEQ_1:sch 2();
F2: l is one-to-one

proof

let i, j be set ; :: according to FUNCT_1:def 8 :: thesis: ( not i in proj1 l or not j in proj1 l or not l . i = l . j or i = j )
assume B1: ( i in dom l & j in dom l & l . i = l . j ) ; :: thesis: i = j
reconsider i = i, j = j as Nat by B1;
( l . i = H₁(i) & l . i = H₁(j) ) by F1, B1;
then i = H₁(j) `2 by MCART_1:7;
hence i = j by MCART_1:7; :: thesis: verum

end;

rng l c= Vars

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng l or z in Vars )
assume z in rng l ; :: thesis: z in Vars
then consider a being set such that
C1: ( a in dom l & z = l . a ) by FUNCT_1:def 5;
reconsider a = a as Nat by C1;
z = H₁(a) by F1, C1;
hence z in Vars by ABCMIZ_1:25; :: thesis: verum

end;

then reconsider l = l as one-to-one FinSequence of Vars by F2, 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 )

proof

let i be Nat; :: thesis: 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 )
let x be variable; :: thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) )
assume ( i in dom l & x = l . i ) ; :: thesis: 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 x = H₁(i) by F1;
hence for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) by MCART_1:7; :: thesis: verum

end;

then reconsider l = l as quasi-loci by ABCMIZ_1:30;
set m = [s,[l,0 ]];
A0: the carrier of MaxConstrSign = {a_Type ,an_Adj ,a_Term } by ABCMIZ_1:def 9;
A1: [s,[l,0 ]] in Constructors by A0, ThCs;
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 A1, ThCc, ABCMIZ_1:def 24;
the_result_sort_of m = m `1 by ABCMIZ_1:def 24
.= s by MCART_1:7 ;
then reconsider m = m as constructor OperSymbol of s by ABCMIZ_1:def 32;
take m ; :: thesis: 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 ) by MCART_1:7
.= card l by MCART_1:7
.= n by F0 ; :: thesis: verum