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 4;
the Sorts of (Free C,(MSVars C)) . s c= Union the Sorts of (Free C,(MSVars C))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (Free C,(MSVars C)) . s or x in Union the Sorts of (Free C,(MSVars C)) )
thus ( not x in the Sorts of (Free C,(MSVars C)) . s or x in Union the Sorts of (Free C,(MSVars C)) ) by A1, CARD_5:10; :: thesis: verum

end;

hence ( z is expression of C,s iff z in the Sorts of (Free C,(MSVars C)) . s ) by Def28; :: thesis: verum