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 object ; :: 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 ) )
reconsider aa = a as set by TARSKI:1;

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: aa = {x} by Th49;
[x,y] in LinTrace f by A2, A3, Th50;
hence [a,y] in Trace g by A1, A3, Th50; :: thesis: verum

end;

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

end;

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