let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C holds
( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) )
let e be expression of C; :: thesis: ( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) )

per cases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) or ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th49;

suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) ; :: thesis: ( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) )

then consider x being Element of Vars such that
A1: ( e = x -term C & e . {} = [x,a_Term ] ) ;
( (e . {} ) `1 = x & (e . {} ) `2 = a_Term ) by A1, MCART_1:7;
hence ( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) ) by A1; :: thesis: verum

end;

suppose ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; :: thesis: ( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) )

then consider o being OperSymbol of C such that
A2: ( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ;
( (e . {} ) `1 = o & (e . {} ) `2 = the carrier of C ) by A2, MCART_1:7;
hence ( ( (e . {} ) `1 in Vars & (e . {} ) `2 = a_Term & e is quasi-term of C ) or ( (e . {} ) `2 = the carrier of C & ( ( (e . {} ) `1 in Constructors & (e . {} ) `1 in the carrier' of C ) or (e . {} ) `1 = * or (e . {} ) `1 = non_op ) ) ) by A2; :: thesis: verum

end;

end;