graph f c= [:C1,(union C2):]
proof
let x be object ; :: 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] and
A2: y in dom f and
A3: z in f . y by Def16;
( rng f c= C2 & f . y in rng f ) by A2, FUNCT_1:def 3, RELAT_1:def 19;
then ( dom f = C1 & z 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 graph f is Subset of [:C1,(union C2):] ; :: thesis: verum