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 r being SortSymbol of S
for y being Element of X . r holds
( x -term is context of y iff ( r = s & x = y ) )
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 r being SortSymbol of S
for y being Element of X . r holds
( x -term is context of y iff ( r = s & x = y ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for r being SortSymbol of S
for y being Element of X . r holds
( x -term is context of y iff ( r = s & x = y ) )
let x be Element of X . s; :: thesis: for r being SortSymbol of S
for y being Element of X . r holds
( x -term is context of y iff ( r = s & x = y ) )
let r be SortSymbol of S; :: thesis: for y being Element of X . r holds
( x -term is context of y iff ( r = s & x = y ) )
let y be Element of X . r; :: thesis: ( x -term is context of y iff ( r = s & x = y ) )
A0: ( ( [x,s] in {[y,r]} implies [x,s] = [y,r] ) & ( [x,s] = [y,r] implies [x,s] in {[y,r]} ) & (x -term) . {} = [x,s] & Coim ((x -term),[y,r]) c= dom (x -term) & dom (x -term) = {{}} & {} in {{}} ) by TARSKI:def 1, TREES_1:29, TREES_4:3, RELAT_1:132;
( ex a being object st Coim ((x -term),[y,r]) = {a} implies Coim ((x -term),[y,r]) = {{}} ) by A0, ZFMISC_1:33;
then ( card (Coim ((x -term),[y,r])) = 1 implies Coim ((x -term),[y,r]) = {{}} ) by CARD_2:42;
hence ( x -term is context of y iff ( r = s & x = y ) ) by A0, CONTEXT, XTUPLE_0:1, FUNCT_1:def 7; :: thesis: verum