set C = MaxConstrSign ;
set m = [a_Type,[{},0]];
set a = [an_Adj,[{},0]];
set f = [a_Term,[{},0]];
A1:
a_Type in {a_Type}
by TARSKI:def 1;
A2:
an_Adj in {an_Adj}
by TARSKI:def 1;
A3:
a_Term in {a_Term}
by TARSKI:def 1;
A4:
[(<*> Vars),0] in [:QuasiLoci,NAT:]
by Th29, ZFMISC_1:def 2;
then A5:
[a_Type,[{},0]] in Modes
by A1, ZFMISC_1:def 2;
A6:
[an_Adj,[{},0]] in Attrs
by A2, A4, ZFMISC_1:def 2;
A7:
[a_Term,[{},0]] in Funcs
by A3, A4, ZFMISC_1:def 2;
A8:
[a_Type,[{},0]] in Modes \/ Attrs
by A5, XBOOLE_0:def 3;
A9:
[an_Adj,[{},0]] in Modes \/ Attrs
by A6, XBOOLE_0:def 3;
A10:
[a_Type,[{},0]] in Constructors
by A8, XBOOLE_0:def 3;
A11:
[an_Adj,[{},0]] in Constructors
by A9, XBOOLE_0:def 3;
A12:
[a_Term,[{},0]] in Constructors
by A7, XBOOLE_0:def 3;
the carrier' of MaxConstrSign = {*,non_op} \/ Constructors
by Def24;
then reconsider m = [a_Type,[{},0]], a = [an_Adj,[{},0]], f = [a_Term,[{},0]] as OperSymbol of MaxConstrSign by A10, A11, A12, XBOOLE_0:def 3;
A13:
m is constructor
;
A14:
a is constructor
;
A15:
f is constructor
;
A16:
the ResultSort of MaxConstrSign . m = m `1
by A13, Def24;
A17:
the ResultSort of MaxConstrSign . a = a `1
by A14, Def24;
A18:
the ResultSort of MaxConstrSign . f = f `1
by A15, Def24;
A19:
the ResultSort of MaxConstrSign . m = a_Type
by A16;
A20:
the ResultSort of MaxConstrSign . a = an_Adj
by A17;
A21:
the ResultSort of MaxConstrSign . f = a_Term
by A18;
A22:
the carrier of MaxConstrSign = {a_Type,an_Adj,a_Term}
by Def9;
let x be object ; TARSKI:def 3,ABCMIZ_1:def 54 ( not x in the carrier of MaxConstrSign or x in rng the ResultSort of MaxConstrSign )
assume
x in the carrier of MaxConstrSign
; x in rng the ResultSort of MaxConstrSign
then
( x = a_Type or x = an_Adj or x = a_Term )
by A22, ENUMSET1:def 1;
hence
x in rng the ResultSort of MaxConstrSign
by A19, A20, A21, FUNCT_2:4; verum