let C be initialized ConstructorSignature; :: thesis: for e being constructor expression of C holds main-constr e in constrs e
let e be constructor expression of C; :: thesis: main-constr e in constrs e
A1: main-constr e = (e . {}) `1 by Def9;
{} in dom e by TREES_1:22;
then e . {} in rng e by FUNCT_1:def 3;
then A2: main-constr e in proj1 (rng e) by A1, MCART_1:86;
main-constr e is constructor OperSymbol of C by Def11;
then main-constr e in { c where c is constructor OperSymbol of C : verum } ;
hence main-constr e in constrs e by A2, XBOOLE_0:def 4; :: thesis: verum