let C1, C2 be Coherence_Space; 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; ( 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
; for a being Element of C1 holds f . a c= g . a
let x be Element of C1; f . x c= g . x
A2:
dom f = C1
by FUNCT_2:def 1;
let z be object ; TARSKI:def 3 ( not z in f . x or z in g . x )
assume
z in f . x
; 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;
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; verum