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 & dom g = C1 ) by FUNCT_2:def 1;
let z be set ; :: 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
A3: ( b is finite & b c= x & z in f . b & ( for c being set st c c= x & z in f . c holds
b c= c ) ) by A2, Th23;
reconsider b = b as Element of C1 by A3, CLASSES1:def 1;

now

let c be set ; :: thesis: ( c in dom f & c c= b & z in f . c implies b = c )
assume A4: ( c in dom f & c c= b & z in f . c ) ; :: thesis: b = c
then c c= x by A3, XBOOLE_1:1;
then b c= c by A3, A4;
hence b = c by A4, XBOOLE_0:def 10; :: thesis: verum

end;

then [b,z] in Trace f by A2, A3, Th32;
then ( z in g . b & g . b c= g . x ) by A1, A2, A3, Def12, Th32;
hence z in g . x ; :: thesis: verum