let C1, C2 be Coherence_Space; :: thesis: for x, y being set st x in union C1 holds
for f being U-linear Function of C1,C2 st LinTrace f = {[x,y]} holds
for a being Element of C1 holds
( ( x in a implies f . a = {y} ) & ( not x in a implies f . a = {} ) )
let a, y be set ; :: thesis: ( a in union C1 implies for f being U-linear Function of C1,C2 st LinTrace f = {[a,y]} holds
for a being Element of C1 holds
( ( a in a implies f . a = {y} ) & ( not a in a implies f . a = {} ) ) )
assume a in union C1 ; :: thesis: for f being U-linear Function of C1,C2 st LinTrace f = {[a,y]} holds
for a being Element of C1 holds
( ( a in a implies f . a = {y} ) & ( not a in a implies f . a = {} ) )
then reconsider a9 = {a} as Element of C1 by COH_SP:4;
let f be U-linear Function of C1,C2; :: thesis: ( LinTrace f = {[a,y]} implies for a being Element of C1 holds
( ( a in a implies f . a = {y} ) & ( not a in a implies f . a = {} ) ) )
assume A1: LinTrace f = {[a,y]} ; :: thesis: for a being Element of C1 holds
( ( a in a implies f . a = {y} ) & ( not a in a implies f . a = {} ) )
let b be Element of C1; :: thesis: ( ( a in b implies f . b = {y} ) & ( not a in b implies f . b = {} ) )
[a,y] in LinTrace f by A1, TARSKI:def 1;
then A2: y in f . {a} by Th52;

hereby :: thesis: ( not a in b implies f . b = {} )

A3: f . b c= {y}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . b or x in {y} )
assume x in f . b ; :: thesis: x in {y}
then consider c being Element of C1 such that
A4: [c,x] in Trace f and
c c= b by Th40;
consider d being set such that
A5: c = {d} by A4, Th49;
[d,x] in LinTrace f by A4, A5, Th50;
then [d,x] = [a,y] by A1, TARSKI:def 1;
then x = y by XTUPLE_0:1;
hence x in {y} by TARSKI:def 1; :: thesis: verum

end;

assume a in b ; :: thesis: f . b = {y}
then A6: a9 c= b by ZFMISC_1:31;
dom f = C1 by FUNCT_2:def 1;
then f . a9 c= f . b by A6, Def11;
then {y} c= f . b by A2, ZFMISC_1:31;
hence f . b = {y} by A3; :: thesis: verum

end;

assume that
A7: not a in b and
A8: f . b <> {} ; :: thesis: contradiction
reconsider B = f . b as non empty set by A8;
set z = the Element of B;
consider c being Element of C1 such that
A9: [c, the Element of B] in Trace f and
A10: c c= b by Th40;
consider d being set such that
A11: c = {d} by A9, Th49;
d in c by A11, TARSKI:def 1;
then A12: d in b by A10;
[d, the Element of B] in LinTrace f by A9, A11, Th50;
then [d, the Element of B] = [a,y] by A1, TARSKI:def 1;
hence contradiction by A7, A12, XTUPLE_0:1; :: thesis: verum