let C1, C2 be Coherence_Space; :: thesis: for x, y being set st x in union C1 & y in union C2 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 & y in union C2 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 & y in union C2 ) ; :: 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 a' = {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 & f . {} = {} ) by A1, Th19, TARSKI:def 1;
then A2: ( {a} in dom f & y in f . {a} ) by Th53;

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

assume a in b ; :: thesis: f . b = {y}
then ( a' c= b & dom f = C1 ) by FUNCT_2:def 1, ZFMISC_1:37;
then f . a' c= f . b by Def12;
then A3: {y} c= f . b by A2, ZFMISC_1:37;
f . b c= {y}

proof

let x be set ; :: 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 & c c= b ) by Th41;
consider d being set such that
A5: c = {d} by A4, Th50;
[d,x] in LinTrace f by A4, A5, Th51;
then [d,x] = [a,y] by A1, TARSKI:def 1;
then x = y by ZFMISC_1:33;
hence x in {y} by TARSKI:def 1; :: thesis: verum

end;

hence f . b = {y} by A3, XBOOLE_0:def 10; :: thesis: verum

end;

assume A6: ( not a in b & f . b <> {} ) ; :: thesis: contradiction
then reconsider B = f . b as non empty set ;
consider z being Element of B;
consider c being Element of C1 such that
A7: ( [c,z] in Trace f & c c= b ) by Th41;
consider d being set such that
A8: c = {d} by A7, Th50;
( [d,z] in LinTrace f & d in c ) by A7, A8, Th51, TARSKI:def 1;
then ( [d,z] = [a,y] & d in b ) by A1, A7, TARSKI:def 1;
hence contradiction by A6, ZFMISC_1:33; :: thesis: verum