let C1, C2 be Coherence_Space; :: thesis:
let f be U-stable Function of C1,C2; :: thesis:
A1: dom f = C1 by FUNCT_2:def 1;

hereby :: thesis:

assume A2: f is U-linear ; :: thesis:
let a be set ; :: thesis:
let y be object ; :: thesis:
assume A3: [a,y] in Trace f ; :: thesis:
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:
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:

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:

let a, y be set ; :: thesis:
assume that
A10: a in dom f and
A11: y in f . a ; :: thesis:
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;

thus b in dom f by A1, A10, A12, CLASSES1:def 1; :: thesis:
let c be set ; :: thesis:
assume that
c in dom f and
A15: c c= b and
A16: y in f . c ; :: thesis:
c c= a by A12, A15;
then b c= c by A14, A16;
hence b = c by A15; :: thesis:

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 b by A17, TARSKI:def 1;
hence ( x in a & y in f . {x} ) by A12, A13, A17; :: thesis:
let c be set ; :: thesis:
assume ( c c= a & y in f . c ) ; :: thesis:
then b c= c by A14;
hence x in c by A17, ZFMISC_1:31; :: thesis:

end;

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