let C1, C2 be Coherence_Space; 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 ; ( 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
; 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; ( 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]}
; 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; ( ( 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 ( not a in b implies f . b = {} )
end;
assume that
A7:
not a in b
and
A8:
f . b <> {}
; 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; verum