let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() 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; for X being V5() 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 V5() 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 Element of X . s; for C being context of x holds x in vf C
let C be context of x; 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; verum