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:10
.= {x} \/ (vars x) by Th27 ; :: thesis: verum