let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
p just_once_values x -context_in p
let s be SortSymbol of S; :: thesis: for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
p just_once_values x -context_in p
let o be OperSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
p just_once_values x -context_in p
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
p just_once_values x -context_in p
let x be Element of X . s; :: thesis: for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds
p just_once_values x -context_in p
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including implies p just_once_values x -context_in p )
set k = p;
set z = x;
assume A0: p is x -context_including ; :: thesis: p just_once_values x -context_in p
Coim (p,(x -context_in p)) = {(x -context_pos_in p)}
proof
thus Coim (p,(x -context_in p)) c= {(x -context_pos_in p)} :: according to XBOOLE_0:def 10 :: thesis: {(x -context_pos_in p)} c= Coim (p,(x -context_in p))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Coim (p,(x -context_in p)) or a in {(x -context_pos_in p)} )
reconsider x = a as set by TARSKI:1;
assume a in Coim (p,(x -context_in p)) ; :: thesis: a in {(x -context_pos_in p)}
then ( x in dom p & p . x in {(x -context_in p)} ) by FUNCT_1:def 7;
then ( x is Nat & p . x = x -context_in p ) by TARSKI:def 1;
then x = x -context_pos_in p by A0, CPI;
hence a in {(x -context_pos_in p)} by TARSKI:def 1; :: thesis: verum
end;
let a be Nat; :: according to MEMBERED:def 12 :: thesis: ( not a in {(x -context_pos_in p)} or a in Coim (p,(x -context_in p)) )
assume a in {(x -context_pos_in p)} ; :: thesis: a in Coim (p,(x -context_in p))
then a = x -context_pos_in p by TARSKI:def 1;
then p . a = x -context_in p by A0, Th71;
then ( a in dom p & p . a in {(x -context_in p)} ) by TARSKI:def 1, FUNCT_1:def 2;
hence a in Coim (p,(x -context_in p)) by FUNCT_1:def 7; :: thesis: verum
end;
hence card (Coim (p,(x -context_in p))) = 1 by CARD_1:30; :: according to FINSEQ_4:def 2 :: thesis: verum