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)))

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:2; :: 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