let C1, C2 be Coherence_Space; :: thesis: for f being cap-distributive Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y being object st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
let f be cap-distributive Function of C1,C2; :: thesis: for a1, a2 being set st a1 \/ a2 in C1 holds
for y being object st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
A1: dom f = C1 by FUNCT_2:def 1;
let a1, a2 be set ; :: thesis: ( a1 \/ a2 in C1 implies for y being object st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2 )
set a = a1 \/ a2;
assume A2: a1 \/ a2 in C1 ; :: thesis: for y being object st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
a2 c= a1 \/ a2 by XBOOLE_1:7;
then A3: a2 in C1 by A2, CLASSES1:def 1;
a1 c= a1 \/ a2 by XBOOLE_1:7;
then A4: a1 in C1 by A2, CLASSES1:def 1;
then reconsider b = a1 /\ a2 as Element of C1 by A3, FINSUB_1:def 2;
b in C1 ;
then A5: C1 includes_lattice_of a1,a2 by A2, A4, A3, Th16;
let y be object ; :: thesis: ( [a1,y] in Trace f & [a2,y] in Trace f implies a1 = a2 )
assume that
A6: [a1,y] in Trace f and
A7: [a2,y] in Trace f ; :: thesis: a1 = a2
( y in f . a1 & y in f . a2 ) by A6, A7, Th31;
then y in (f . a1) /\ (f . a2) by XBOOLE_0:def 4;
then A8: y in f . b by A1, A5, Def12;
b c= a1 by XBOOLE_1:17;
then ( b c= a2 & b = a1 ) by A1, A6, A8, Th31, XBOOLE_1:17;
hence a1 = a2 by A1, A7, A8, Th31; :: thesis: verum