let C be initialized ConstructorSignature; :: thesis: for x being variable holds vars (x -term C) = {x} \/ (vars x)
let x be variable; :: thesis: vars (x -term C) = {x} \/ (vars x)
thus vars (x -term C) = varcl {x} by MSAFREE3:11
.= {x} \/ (vars x) by Th82 ; :: thesis: verum