let C be initialized ConstructorSignature; :: thesis: for e being expression of C
for f being empty valuation of C holds e at f = e
let e be expression of C; :: thesis: for f being empty valuation of C holds e at f = e
let f be empty valuation of C; :: thesis: e at f = e
f = C idval ({} Vars) ;
hence e at f = e by Th137; :: thesis: verum