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))))
A1: dom (f #) = Union the Sorts of (Free (C,(MSVars C))) by FUNCT_2:def 1;

now :: thesis: for x being object st x in Union the Sorts of (Free (C,(MSVars C))) holds
(f #) . x = x

let x be object ; :: 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 Th139 ; :: thesis: verum

end;

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