let C be initialized ConstructorSignature; :: thesis: for f being empty valuation of C holds f # = id (Union the Sorts of (Free C,(MSVars C)))
let f be empty valuation of C; :: thesis: f # = id (Union the Sorts of (Free C,(MSVars C)))
A0: dom (f # ) = Union the Sorts of (Free C,(MSVars C)) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in Union the Sorts of (Free C,(MSVars C)) implies (f # ) . x = x )
assume x in Union the Sorts of (Free C,(MSVars C)) ; :: thesis: (f # ) . x = x
then reconsider t = x as expression of C ;
thus (f # ) . x = t at f
.= x by ThS2 ; :: thesis: verum

end;

hence f # = id (Union the Sorts of (Free C,(MSVars C))) by A0, FUNCT_1:34; :: thesis: verum