let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2 holds Trace f c= [:(Sub_of_Fin C1),(union C2):]
let f be U-stable Function of C1,C2; :: thesis: Trace f c= [:(Sub_of_Fin C1),(union C2):]
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in Trace f or [x1,x2] in [:(Sub_of_Fin C1),(union C2):] )
assume A1: [x1,x2] in Trace f ; :: thesis: [x1,x2] in [:(Sub_of_Fin C1),(union C2):]
then consider a, y being set such that
A2: [x1,x2] = [a,y] and
A3: a in dom f and
A4: y in f . a and
for b being set st b in dom f & b c= a & y in f . b holds
a = b by Def17;
A5: dom f = C1 by FUNCT_2:def 1;
then a is finite by A1, A2, Th33;
then A6: a in Sub_of_Fin C1 by A3, A5, Def3;
y in union C2 by A3, A4, A5, Lm1;
hence [x1,x2] in [:(Sub_of_Fin C1),(union C2):] by A2, A6, ZFMISC_1:87; :: thesis: verum