let C1, C2 be Coherence_Space; :: thesis: for f, g being U-stable Function of C1,C2 st Trace f c= Trace g holds
for a being Element of C1 holds f . a c= g . a
let f, g be U-stable Function of C1,C2; :: thesis: ( Trace f c= Trace g implies for a being Element of C1 holds f . a c= g . a )
assume A1: Trace f c= Trace g ; :: thesis: for a being Element of C1 holds f . a c= g . a
let x be Element of C1; :: thesis: f . x c= g . x
A2: dom f = C1 by FUNCT_2:def 1;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f . x or z in g . x )
assume z in f . x ; :: thesis: z in g . x
then consider b being set such that
b is finite and
A3: b c= x and
A4: z in f . b and
A5: for c being set st c c= x & z in f . c holds
b c= c by A2, Th22;
reconsider b = b as Element of C1 by A3, CLASSES1:def 1;

now :: thesis: for c being set st c in dom f & c c= b & z in f . c holds
b = c

let c be set ; :: thesis: ( c in dom f & c c= b & z in f . c implies b = c )
assume that
c in dom f and
A6: c c= b and
A7: z in f . c ; :: thesis: b = c
c c= x by A3, A6;
then b c= c by A5, A7;
hence b = c by A6; :: thesis: verum

end;

then [b,z] in Trace f by A2, A4, Th31;
then A8: z in g . b by A1, Th31;
dom g = C1 by FUNCT_2:def 1;
then g . b c= g . x by A3, Def11;
hence z in g . x by A8; :: thesis: verum