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
consider X being empty Subset of Vars ;
f = C idval X ;
hence e at f = e by Th137; :: thesis: verum