let z be set ; :: thesis: for C being initialized ConstructorSignature
for s being SortSymbol of C holds
( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )
let C be initialized ConstructorSignature; :: thesis: for s being SortSymbol of C holds
( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )
let s be SortSymbol of C; :: thesis: ( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )
A1: dom the Sorts of (Free (C,(MSVars C))) = the carrier of C by PARTFUN1:def 2;
the Sorts of (Free (C,(MSVars C))) . s c= Union the Sorts of (Free (C,(MSVars C))) by A1, CARD_5:2;
hence ( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s ) by Def28; :: thesis: verum