let C be initialized ConstructorSignature; :: thesis: for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))
let X be Subset of Vars; :: thesis: (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))
set f = C idval X;
A1: dom ((C idval X) #) = 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
((C idval X) #) . x = x

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

end;

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