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 )
A1: dom f = C1 by FUNCT_2:def 1;
A2: dom g = C1 by FUNCT_2:def 1;
A3: now :: thesis: for a being Element of C1
for f, g being U-stable Function of C1,C2 st Trace f = Trace g holds
f .: (Fin a) c= g .: (Fin a)
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) )
A4: dom g = C1 by FUNCT_2:def 1;
assume A5: Trace f = Trace g ; :: thesis: f .: (Fin a) c= g .: (Fin a)
thus f .: (Fin a) c= g .: (Fin a) :: thesis: verum
proof
let y be object ; :: 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 object such that
x in dom f and
A6: x in Fin a and
A7: y = f . x by FUNCT_1:def 6;
( f . x c= g . x & g . x c= f . x ) by A5, A6, Th36;
then f . x = g . x ;
hence y in g .: (Fin a) by A4, A6, A7, FUNCT_1:def 6; :: thesis: verum
end;
end;
assume A8: Trace f = Trace g ; :: thesis: f = g
now :: thesis: for a being Element of C1 holds f . a = g . a
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 A8, A3;
then A9: f .: (Fin a) = g .: (Fin a) ;
thus f . a = union (f .: (Fin a)) by A1, Th20
.= g . a by A2, A9, Th20 ; :: thesis: verum
end;
hence f = g by FUNCT_2:63; :: thesis: verum