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 that
A1: o <> * and
A2: 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;
A3: len ((len (the_arity_of o)) |-> a_Term) = len (the_arity_of o) by CARD_1:def 7;
A4: the_arity_of o in {a_Term} * by A1, A2, Def9;
(len (the_arity_of o)) |-> t in {a_Term} * by FINSEQ_1:def 11;
hence the_arity_of o = (len (the_arity_of o)) |-> a_Term by A3, A4, Th6; :: thesis: verum