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 ) ;
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;
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