let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2 holds
( f is U-linear iff for a being set
for y being object st [a,y] in Trace f holds
ex x being set st a = {x} )
let f be U-stable Function of C1,C2; :: thesis: ( f is U-linear iff for a being set
for y being object st [a,y] in Trace f holds
ex x being set st a = {x} )
A1: dom f = C1 by FUNCT_2:def 1;

hereby :: thesis: ( ( for a being set
for y being object st [a,y] in Trace f holds
ex x being set st a = {x} ) implies f is U-linear )

assume A2: f is U-linear ; :: thesis: for a being set
for y being object st [a,y] in Trace f holds
ex x being set st a = {x}
let a be set ; :: thesis: for y being object st [a,y] in Trace f holds
ex x being set st a = {x}
let y be object ; :: thesis: ( [a,y] in Trace f implies ex x being set st a = {x} )
assume A3: [a,y] in Trace f ; :: thesis: ex x being set st a = {x}
then A4: a in dom f by Th31;
y in f . a by A3, Th31;
then consider x being set such that
A5: x in a and
A6: y in f . {x} and
for b being set st b c= a & y in f . b holds
x in b by A1, A2, A4, Th23;
A7: {x} c= a by A5, ZFMISC_1:31;
take x = x; :: thesis: a = {x}
A8: {x,x} = {x} by ENUMSET1:29;
{x,x} in C1 by A1, A4, A5, COH_SP:6;
hence a = {x} by A1, A3, A6, A7, A8, Th31; :: thesis: verum

end;

assume A9: for a being set
for y being object st [a,y] in Trace f holds
ex x being set st a = {x} ; :: thesis: f is U-linear

now :: thesis: for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )

let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) ) )
assume that
A10: a in dom f and
A11: y in f . a ; :: thesis: ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )
consider b being set such that
b is finite and
A12: b c= a and
A13: y in f . b and
A14: for c being set st c c= a & y in f . c holds
b c= c by A1, A10, A11, Th22;

now :: thesis: ( b in dom f & ( for c being set st c in dom f & c c= b & y in f . c holds
b = c ) )

thus b in dom f by A1, A10, A12, CLASSES1:def 1; :: 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
A15: c c= b and
A16: y in f . c ; :: thesis: b = c
c c= a by A12, A15;
then b c= c by A14, A16;
hence b = c by A15; :: thesis: verum

end;

then [b,y] in Trace f by A13, Th31;
then consider x being set such that
A17: b = {x} by A9;
take x = x; :: thesis: ( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )
x in b by A17, TARSKI:def 1;
hence ( x in a & y in f . {x} ) by A12, A13, A17; :: thesis: for c being set st c c= a & y in f . c holds
x in c
let c be set ; :: thesis: ( c c= a & y in f . c implies x in c )
assume ( c c= a & y in f . c ) ; :: thesis: x in c
then b c= c by A14;
hence x in c by A17, ZFMISC_1:31; :: thesis: verum

end;

hence f is U-linear by A1, Th23; :: thesis: verum