let C1, C2 be Coherence_Space; :: thesis:
let X be Subset of [:C1,(union C2):]; :: thesis:
assume that
A1: for x being set st x in X holds
x `1 is finite and
A2: for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 and
A3: for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ; :: thesis:
deffunc H₁( set ) -> set = X .: (Fin $1);
consider f being Function such that
A4: ( dom f = C1 & ( for a being set st a in C1 holds
f . a = H₁(a) ) ) from FUNCT_1:sch 5();

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume x in rng f ; :: thesis:
then consider a being object such that
A18: a in dom f and
A19: x = f . a by FUNCT_1:def 3;
reconsider a = a as Element of C1 by A4, A18;
A20: x = X .: (Fin a) by A4, A19;

let z, y be set ; :: thesis:
assume z in xx ; :: thesis:
then consider z1 being object such that
A21: [z1,z] in X and
A22: z1 in Fin a by A20, RELAT_1:def 13;
assume y in xx ; :: thesis:
then consider y1 being object such that
A23: [y1,y] in X and
A24: y1 in Fin a by A20, RELAT_1:def 13;
reconsider y1 = y1, z1 = z1 as set by TARSKI:1;
z1 \/ y1 in Fin a by A22, A24, FINSUB_1:1;
hence {z,y} in C2 by A2, A21, A22, A23, A24; :: thesis:

end;

end;

let a, b be set ; :: according to COHSP_1:def 11 :: thesis:
assume that
A25: ( a in dom f & b in dom f ) and
A26: a c= b ; :: thesis:
reconsider a = a, b = b as Element of C1 by A4, A25;
Fin a c= Fin b by A26, FINSUB_1:10;
then A27: X .: (Fin a) c= X .: (Fin b) by RELAT_1:123;
f . a = X .: (Fin a) by A4;
hence f . a c= f . b by A4, A27; :: thesis:

end;

let a, b be object ; :: according to RELAT_1:def 2 :: thesis:

let c be set ; :: thesis:
assume that
A31: c in dom f and
A32: c c= a9 and
A33: b in f . c ; :: thesis:
reconsider c9 = c as Element of C1 by A4, A31;
b in X .: (Fin c9) by A4, A33;
then consider x being object such that
A34: [x,b] in X and
A35: x in Fin c9 by RELAT_1:def 13;
reconsider x = x as set by TARSKI:1;
A36: x c= c by A35, FINSUB_1:def 5;
then x \/ a9 = a9 by A32, XBOOLE_1:1, XBOOLE_1:12;
then x = a by A3, A28, A34, A35;
hence a9 = c by A32, A36; :: thesis:

end;

f . a9 = X .: (Fin a9) by A4;
hence [a,b] in Trace f by A4, A29, A30, Th31; :: thesis:

end;

assume A37: [a,b] in Trace f ; :: thesis:
reconsider a = a, b = b as set by TARSKI:1;
( a in dom f & b in f . a ) by Th31, A37;
then b in X .: (Fin a) by A4;
then consider x being object such that
A38: [x,b] in X and
A39: x in Fin a by RELAT_1:def 13;
reconsider a = a as Element of C1 by A4, A37, Th31;
x in Fin a by A39;
then reconsider x = x as finite Element of C1 ;
x in Fin x by FINSUB_1:def 5;
then b in X .: (Fin x) by A38, RELAT_1:def 13;
then A40: b in f . x by A4;
x c= a by A39, FINSUB_1:def 5;
hence [a,b] in X by A4, A37, A38, A40, Th31; :: thesis:

end;