let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2
for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
let f be U-stable Function of C1,C2; :: thesis: for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
let a be Element of C1; :: thesis: for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
let y be set ; :: thesis: ( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
A1: dom f = C1 by FUNCT_2:def 1;
hereby :: thesis: ( ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) implies y in f . a )
assume y in f . a ; :: thesis: ex b being Element of C1 st
( [b,y] in Trace f & b c= a )
then consider b being set such that
b is finite and
A2: b c= a and
A3: y in f . b and
A4: for c being set st c c= a & y in f . c holds
b c= c by A1, Th22;
reconsider b = b as Element of C1 by A2, CLASSES1:def 1;
take b = b; :: thesis: ( [b,y] in Trace f & b c= a )
now :: thesis: for c being set st c in dom f & c c= b & y in f . c holds
b = c
let c be set ; :: thesis: ( c in dom f & c c= b & y in f . c implies b = c )
assume that
c in dom f and
A5: c c= b and
A6: y in f . c ; :: thesis: b = c
c c= a by A2, A5;
then b c= c by A4, A6;
hence b = c by A5; :: thesis: verum
end;
hence [b,y] in Trace f by A1, A3, Th31; :: thesis: b c= a
thus b c= a by A2; :: thesis: verum
end;
given b being Element of C1 such that A7: [b,y] in Trace f and
A8: b c= a ; :: thesis: y in f . a
A9: y in f . b by A7, Th31;
f . b c= f . a by A1, A8, Def11;
hence y in f . a by A9; :: thesis: verum