let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s holds vf (x -term) = {x}
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s holds vf (x -term) = {x}
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s holds vf (x -term) = {x}
let x be Element of X . s; :: thesis: vf (x -term) = {x}
A1: rng (x -term) = {[x,s]} by FUNCOP_1:8;
rng (x -term) c= [:(Union X), the carrier of S:] by A1, ZFMISC_1:31, ZFMISC_1:87;
then (rng (x -term)) /\ [:(Union X), the carrier of S:] = rng (x -term) by XBOOLE_1:28;
hence vf (x -term) = {x} by A1, RELAT_1:9; :: thesis: verum