let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C holds
( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
let e be expression of C; :: thesis: ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
A1: ( (e . {}) `1 in Vars or (e . {}) `1 in the carrier' of C or (e . {}) `1 = ast C or (e . {}) `1 = non_op C ) by Th14;
Vars misses the carrier' of C by Th10;
hence ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) by A1, XBOOLE_0:3; :: thesis: verum