let C1, C2 be Coherence_Space; :: thesis: for a being Element of C1
for y being set
for f being U-stable Function of C1,C2 st Trace f = {[a,y]} holds
for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )
let a be Element of C1; :: thesis: for y being set
for f being U-stable Function of C1,C2 st Trace f = {[a,y]} holds
for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )
let y be set ; :: thesis: for f being U-stable Function of C1,C2 st Trace f = {[a,y]} holds
for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )
let f be U-stable Function of C1,C2; :: thesis: ( Trace f = {[a,y]} implies for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) ) )
assume A1: Trace f = {[a,y]} ; :: thesis: for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )
let b be Element of C1; :: thesis: ( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )
A2: [a,y] in Trace f by A1, TARSKI:def 1;

hereby :: thesis: ( not a c= b implies f . b = {} )

A3: f . b c= {y}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . b or x in {y} )
assume x in f . b ; :: thesis: x in {y}
then consider c being Element of C1 such that
A4: [c,x] in Trace f and
c c= b by Th40;
[c,x] = [a,y] by A1, A4, TARSKI:def 1;
then x = y by XTUPLE_0:1;
hence x in {y} by TARSKI:def 1; :: thesis: verum

end;

assume a c= b ; :: thesis: f . b = {y}
then y in f . b by A2, Th40;
then {y} c= f . b by ZFMISC_1:31;
hence f . b = {y} by A3; :: thesis: verum

end;

assume that
A5: not a c= b and
A6: f . b <> {} ; :: thesis: contradiction
reconsider B = f . b as non empty set by A6;
set z = the Element of B;
consider c being Element of C1 such that
A7: [c, the Element of B] in Trace f and
A8: c c= b by Th40;
[c, the Element of B] = [a,y] by A1, A7, TARSKI:def 1;
hence contradiction by A5, A8, XTUPLE_0:1; :: thesis: verum