let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2 holds
( f is U-linear iff for a, y being set 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, y being set 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, y being set 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, y being set st [a,y] in Trace f holds
ex x being set st a = {x}
let a, y be set ; :: 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 & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Th32;
then consider x being set such that
A5: ( x in a & y in f . {x} & ( for b being set st b c= a & y in f . b holds
x in b ) ) by A1, A2, Th24;
take x = x; :: thesis: a = {x}
( {x} c= a & {x,x} in C1 & {x,x} = {x} ) by A1, A4, A5, COH_SP:6, ENUMSET1:69, ZFMISC_1:37;
hence a = {x} by A1, A3, A5, Th32; :: thesis: verum

end;

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

now

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 A7: ( a in dom f & 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 ) )
then consider b being set such that
A8: ( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) by A1, Th23;

now

thus b in dom f by A1, A7, A8, 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 A9: ( c in dom f & c c= b & y in f . c ) ; :: thesis: b = c
then c c= a by A8, XBOOLE_1:1;
then b c= c by A8, A9;
hence b = c by A9, XBOOLE_0:def 10; :: thesis: verum

end;

then [b,y] in Trace f by A8, Th32;
then consider x being set such that
A10: b = {x} by A6;
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 A10, TARSKI:def 1;
hence ( x in a & y in f . {x} ) by A8, A10; :: 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 A8;
hence x in c by A10, ZFMISC_1:37; :: thesis: verum

end;

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