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 = {} )

assume a c= b ; :: thesis: f . b = {y}
then y in f . b by A2, Th41;
then A3: {y} c= f . b by ZFMISC_1:37;
f . b c= {y}

proof

let x be set ; :: 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 & c c= b ) by Th41;
[c,x] = [a,y] by A1, A4, TARSKI:def 1;
then x = y by ZFMISC_1:33;
hence x in {y} by TARSKI:def 1; :: thesis: verum

end;

hence f . b = {y} by A3, XBOOLE_0:def 10; :: thesis: verum

end;

assume A5: ( not a c= b & f . b <> {} ) ; :: thesis: contradiction
then reconsider B = f . b as non empty set ;
consider z being Element of B;
consider c being Element of C1 such that
A6: ( [c,z] in Trace f & c c= b ) by Th41;
[c,z] = [a,y] by A1, A6, TARSKI:def 1;
hence contradiction by A5, A6, ZFMISC_1:33; :: thesis: verum