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

let x be set ; :: 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:34; :: thesis: verum