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 set ; :: 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] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Def18;
A3: dom f = C1 by FUNCT_2:def 1;
then a is finite by A1, A2, Th34;
then ( a in Sub_of_Fin C1 & y in union C2 ) by A2, A3, Def3, Lm1;
hence [x1,x2] in [:(Sub_of_Fin C1),(union C2):] by A2, ZFMISC_1:106; :: thesis: verum