let S be ConstructorSignature; :: thesis: for o being OperSymbol of S st o is constructor holds
the_arity_of o = (len (the_arity_of o)) |-> a_Term
let o be OperSymbol of S; :: thesis: ( o is constructor implies the_arity_of o = (len (the_arity_of o)) |-> a_Term )
assume A1: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def 11 :: thesis: the_arity_of o = (len (the_arity_of o)) |-> a_Term
reconsider t = a_Term as Element of {a_Term } by TARSKI:def 1;
( len ((len (the_arity_of o)) |-> a_Term ) = len (the_arity_of o) & the_arity_of o in {a_Term } * & (len (the_arity_of o)) |-> t in {a_Term } * ) by A1, CONSTRSIGN, FINSEQ_1:def 11, FINSEQ_1:def 18;
hence the_arity_of o = (len (the_arity_of o)) |-> a_Term by Th1A; :: thesis: verum