let C1, C2 be Coherence_Space; :: thesis: for f, g being U-linear Function of C1,C2 st LinTrace f = LinTrace g holds
f = g
let f, g be U-linear Function of C1,C2; :: thesis: ( LinTrace f = LinTrace g implies f = g )
assume A1: LinTrace f = LinTrace g ; :: thesis: f = g
Trace f = Trace g

proof

let a, y be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,y] in Trace f or [a,y] in Trace g ) & ( not [a,y] in Trace g or [a,y] in Trace f ) )

hereby :: thesis: ( not [a,y] in Trace g or [a,y] in Trace f )

assume A2: [a,y] in Trace f ; :: thesis: [a,y] in Trace g
then consider x being set such that
A3: a = {x} by Th50;
[x,y] in LinTrace f by A2, A3, Th51;
hence [a,y] in Trace g by A1, A3, Th51; :: thesis: verum

end;

assume A4: [a,y] in Trace g ; :: thesis: [a,y] in Trace f
then consider x being set such that
A5: a = {x} by Th50;
[x,y] in LinTrace g by A4, A5, Th51;
hence [a,y] in Trace f by A1, A5, Th51; :: thesis: verum

end;

hence f = g by Th38; :: thesis: verum