Trace f c= [:C1,(union C2):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Trace f or x in [:C1,(union C2):] )
assume x in Trace f ; :: thesis: x in [:C1,(union C2):]
then consider a, y being set such that
A1: x = [a,y] and
A2: a in dom f and
A3: y in f . a and
for b being set st b in dom f & b c= a & y in f . b holds
a = b by Def17;
( rng f c= C2 & f . a in rng f ) by A2, FUNCT_1:def 3, RELAT_1:def 19;
then ( dom f = C1 & y in union C2 ) by A3, FUNCT_2:def 1, TARSKI:def 4;
hence x in [:C1,(union C2):] by A1, A2, ZFMISC_1:87; :: thesis: verum

end;

hence Trace f is Subset of [:C1,(union C2):] ; :: thesis: verum