let C1, C2 be Coherence_Space; :: thesis: for f, g being U-stable Function of C1,C2 st Trace f = Trace g holds
f = g
let f, g be U-stable Function of C1,C2; :: thesis: ( Trace f = Trace g implies f = g )
assume A1: Trace f = Trace g ; :: thesis: f = g
A2: ( dom f = C1 & dom g = C1 ) by FUNCT_2:def 1;

A3: now

let a be Element of C1; :: thesis: for f, g being U-stable Function of C1,C2 st Trace f = Trace g holds
f .: (Fin a) c= g .: (Fin a)
let f, g be U-stable Function of C1,C2; :: thesis: ( Trace f = Trace g implies f .: (Fin a) c= g .: (Fin a) )
assume A4: Trace f = Trace g ; :: thesis: f .: (Fin a) c= g .: (Fin a)
A5: ( dom f = C1 & dom g = C1 ) by FUNCT_2:def 1;
thus f .: (Fin a) c= g .: (Fin a) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Fin a) or y in g .: (Fin a) )
assume y in f .: (Fin a) ; :: thesis: y in g .: (Fin a)
then consider x being set such that
A6: ( x in dom f & x in Fin a & y = f . x ) by FUNCT_1:def 12;
( f . x c= g . x & g . x c= f . x ) by A4, A6, Th37;
then f . x = g . x by XBOOLE_0:def 10;
hence y in g .: (Fin a) by A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

end;

now

let a be Element of C1; :: thesis: f . a = g . a
( f .: (Fin a) c= g .: (Fin a) & g .: (Fin a) c= f .: (Fin a) ) by A1, A3;
then A7: f .: (Fin a) = g .: (Fin a) by XBOOLE_0:def 10;
thus f . a = union (f .: (Fin a)) by A2, Th21
.= g . a by A2, A7, Th21 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum