let C be ConstructorSignature; :: thesis: ( C is standardized iff C is Subsignature of MaxConstrSign )
A4: the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors by ABCMIZ_1:def 24;
A5: dom the Arity of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def 1;
A6: dom the ResultSort of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def 1;
thus ( C is standardized implies C is Subsignature of MaxConstrSign ) :: thesis: ( C is Subsignature of MaxConstrSign implies C is standardized )

proof

assume A1: for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) ) ; :: according to ABCMIZ_A:def 1 :: thesis: C is Subsignature of MaxConstrSign
A2: ( the carrier of C = 3 & the carrier of MaxConstrSign = 3 ) by ABCMIZ_1:def 9, YELLOW11:1;
A3: the Arity of C c= the Arity of MaxConstrSign

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the Arity of C or [x,y] in the Arity of MaxConstrSign )
assume B1: [x,y] in the Arity of C ; :: thesis: [x,y] in the Arity of MaxConstrSign
then reconsider x = x as OperSymbol of C by ZFMISC_1:106;
( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def 11;
then ( x in {* ,non_op } or x in Constructors ) by A1, TARSKI:def 2;
then reconsider c = x as OperSymbol of MaxConstrSign by A4, XBOOLE_0:def 3;
B2: y = the Arity of C . x by B1, FUNCT_1:8;

per cases ( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def 11;

suppose ( x = * or x = non_op ) ; :: thesis: [x,y] in the Arity of MaxConstrSign

then ( ( c = * & y = <*an_Adj ,a_Type *> ) or ( c = non_op & y = <*an_Adj *> ) ) by B2, ABCMIZ_1:def 9;
then y = the Arity of MaxConstrSign . c by ABCMIZ_1:def 9;
hence [x,y] in the Arity of MaxConstrSign by A5, FUNCT_1:def 4; :: thesis: verum

end;

suppose B3: x is constructor ; :: thesis: [x,y] in the Arity of MaxConstrSign

then B6: ( x <> * & x <> non_op ) by ABCMIZ_1:def 11;
then B5: c is constructor by ABCMIZ_1:def 11;
card ((x `2 ) `1 ) = len (the_arity_of x) by A1, B3
.= card y by B1, FUNCT_1:8 ;
then B4: card y = card (the Arity of MaxConstrSign . c) by B5, ABCMIZ_1:def 24;
( y in {a_Term } * & the Arity of MaxConstrSign . c in {a_Term } * ) by B2, B6, ABCMIZ_1:def 9;
then y = the Arity of MaxConstrSign . c by B4, ABCMIZ_1:6;
hence [x,y] in the Arity of MaxConstrSign by A5, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

the ResultSort of C c= the ResultSort of MaxConstrSign

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the ResultSort of C or [x,y] in the ResultSort of MaxConstrSign )
assume B1: [x,y] in the ResultSort of C ; :: thesis: [x,y] in the ResultSort of MaxConstrSign
then reconsider x = x as OperSymbol of C by ZFMISC_1:106;
( x is constructor or x = * or x = non_op ) by ABCMIZ_1:def 11;
then ( x in {* ,non_op } or x in Constructors ) by A1, TARSKI:def 2;
then reconsider c = x as OperSymbol of MaxConstrSign by A4, XBOOLE_0:def 3;
B2: y = the ResultSort of C . x by B1, FUNCT_1:8;

per cases ( x = * or x = non_op or ( x is constructor & c is constructor ) ) by ABCMIZ_1:def 11;

suppose ( x = * or x = non_op ) ; :: thesis: [x,y] in the ResultSort of MaxConstrSign

then ( ( c = * & y = a_Type ) or ( c = non_op & y = an_Adj ) ) by B2, ABCMIZ_1:def 9;
then y = the ResultSort of MaxConstrSign . c by ABCMIZ_1:def 9;
hence [x,y] in the ResultSort of MaxConstrSign by A6, FUNCT_1:def 4; :: thesis: verum

end;

suppose B3: ( x is constructor & c is constructor ) ; :: thesis: [x,y] in the ResultSort of MaxConstrSign

then x `1 = the_result_sort_of x by A1
.= y by B1, FUNCT_1:8 ;
then y = the_result_sort_of c by B3, StandardizedDef
.= the ResultSort of MaxConstrSign . c ;
hence [x,y] in the ResultSort of MaxConstrSign by A6, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence C is Subsignature of MaxConstrSign by A2, A3, INSTALG1:14; :: thesis: verum

end;

assume C1: C is Subsignature of MaxConstrSign ; :: thesis: C is standardized
let o be OperSymbol of C; :: according to ABCMIZ_A:def 1 :: thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) ) )
assume C2: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def 11 :: thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) )
( the carrier' of C c= the carrier' of MaxConstrSign & o in the carrier' of C ) by C1, INSTALG1:11;
then reconsider c = o as OperSymbol of MaxConstrSign ;
C3: c is constructor by C2, ABCMIZ_1:def 11;
not c in {* ,non_op } by C2, TARSKI:def 2;
hence o in Constructors by A4, XBOOLE_0:def 3; :: thesis: ( o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) )
thus o `1 = the ResultSort of MaxConstrSign . c by C3, ABCMIZ_1:def 24
.= (the ResultSort of MaxConstrSign | the carrier' of C) . o by FUNCT_1:72
.= the ResultSort of C . o by C1, INSTALG1:13
.= the_result_sort_of o ; :: thesis: card ((o `2 ) `1 ) = len (the_arity_of o)
thus card ((o `2 ) `1 ) = card (the Arity of MaxConstrSign . c) by C3, ABCMIZ_1:def 24
.= card ((the Arity of MaxConstrSign | the carrier' of C) . o) by FUNCT_1:72
.= card (the Arity of C . o) by C1, INSTALG1:13
.= len (the_arity_of o) ; :: thesis: verum