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 MCON;
{} in dom e by TREES_1:47;
then e . {} in rng e by FUNCT_1:def 5;
then A2: main-constr e in proj1 (rng e) by A1, MCART_1:91;
main-constr e is constructor OperSymbol of C by CONSTR;
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