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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in graph f or x in [:C1,(union C2):] )
assume x in graph f ; :: thesis: x in [:C1,(union C2):]
then consider y being finite set , z being set such that
A1: ( x = [y,z] & y in dom f & z in f . y ) by Def17;
A2: ( dom f = C1 & rng f c= C2 ) by FUNCT_2:def 1, RELAT_1:def 19;
f . y in rng f by A1, FUNCT_1:def 5;
then z in union C2 by A1, A2, TARSKI:def 4;
hence x in [:C1,(union C2):] by A1, A2, ZFMISC_1:106; :: thesis: verum

end;

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