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
for C being context of x holds x in vf C
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
for C being context of x holds x in vf C
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for C being context of x holds x in vf C
let x be Element of X . s; :: thesis: for C being context of x holds x in vf C
let C be context of x; :: thesis: x in vf C
card (Coim (C,[x,s])) = 1 by CONTEXT;
then consider a being object such that
A1: Coim (C,[x,s]) = {a} by CARD_2:42;
a in {a} by TARSKI:def 1;
then ( a in dom C & C . a in {[x,s]} ) by A1, FUNCT_1:def 7;
then A2: ( [x,s] = C . a & C . a in rng C ) by TARSKI:def 1, FUNCT_1:def 3;
[x,s] in [:(Union X), the carrier of S:] by ZFMISC_1:87;
then [x,s] in (rng C) /\ [:(Union X), the carrier of S:] by A2, XBOOLE_0:def 4;
hence x in vf C by XTUPLE_0:def 12; :: thesis: verum