let C1, C2 be Coherence_Space; 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; ( LinTrace f = LinTrace g implies f = g )
assume A1:
LinTrace f = LinTrace g
; f = g
Trace f = Trace g
proof
let a,
y be
object ;
RELAT_1:def 2 ( ( 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;
assume A4:
[a,y] in Trace g
;
[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;
verum
end;
hence
f = g
by Th37; verum