let C be ConstructorSignature; :: thesis: ( C is standardized iff C is Subsignature of MaxConstrSign )
A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def 24;
A2: dom the Arity of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def 1;
A3: 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 A4: 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
A5: ( the carrier of C = 3 & the carrier of MaxConstrSign = 3 ) by ABCMIZ_1:def 9, YELLOW11:1;
A6: the Arity of C c= the Arity of MaxConstrSign

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the Arity of C or [x,y] in the Arity of MaxConstrSign )
assume A7: [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:87;
( x = * or x = non_op or x is constructor ) ;
then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def 2;
then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def 3;
A8: y = the Arity of C . x by A7, FUNCT_1:1;

per cases ( x = * or x = non_op or x is constructor ) ;

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 A8, 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 A2, FUNCT_1:def 2; :: thesis: verum

end;

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

then A10: ( x <> * & x <> non_op ) ;
then A11: c is constructor ;
reconsider y = y as set by TARSKI:1;
card ((x `2) `1) = len (the_arity_of x) by A4, A9
.= card y by A7, FUNCT_1:1 ;
then A12: card y = card ( the Arity of MaxConstrSign . c) by A11, ABCMIZ_1:def 24;
( y in {a_Term} * & the Arity of MaxConstrSign . c in {a_Term} * ) by A8, A10, ABCMIZ_1:def 9;
then y = the Arity of MaxConstrSign . c by A12, ABCMIZ_1:6;
hence [x,y] in the Arity of MaxConstrSign by A2, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

the ResultSort of C c= the ResultSort of MaxConstrSign

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the ResultSort of C or [x,y] in the ResultSort of MaxConstrSign )
assume A13: [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:87;
( x is constructor or x = * or x = non_op ) ;
then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def 2;
then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def 3;
A14: y = the ResultSort of C . x by A13, FUNCT_1:1;

per cases ( x = * or x = non_op or ( x is constructor & c is constructor ) ) ;

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 A14, 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 A3, FUNCT_1:def 2; :: thesis: verum

end;

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

then x `1 = the_result_sort_of x by A4
.= y by A13, FUNCT_1:1 ;
then y = the_result_sort_of c by A15, Def1
.= the ResultSort of MaxConstrSign . c ;
hence [x,y] in the ResultSort of MaxConstrSign by A3, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence C is Subsignature of MaxConstrSign by A5, A6, INSTALG1:13; :: thesis: verum

end;

assume A16: 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 A17: ( 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 A16, INSTALG1:10;
then reconsider c = o as OperSymbol of MaxConstrSign ;
A18: c is constructor by A17;
not c in {*,non_op} by A17, TARSKI:def 2;
hence o in Constructors by A1, 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 A18, ABCMIZ_1:def 24
.= ( the ResultSort of MaxConstrSign | the carrier' of C) . o by FUNCT_1:49
.= the ResultSort of C . o by A16, INSTALG1:12
.= 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 A18, ABCMIZ_1:def 24
.= card (( the Arity of MaxConstrSign | the carrier' of C) . o) by FUNCT_1:49
.= card ( the Arity of C . o) by A16, INSTALG1:12
.= len (the_arity_of o) ; :: thesis: verum