set f = id (union C);

now :: thesis: for x, y being set st {x,y} in C holds
{((id (union C)) . x),((id (union C)) . y)} in C

let x, y be set ; :: thesis: ( {x,y} in C implies {((id (union C)) . x),((id (union C)) . y)} in C )
assume A1: {x,y} in C ; :: thesis: {((id (union C)) . x),((id (union C)) . y)} in C
then x in union C by Th16;
then A2: (id (union C)) . x = x by FUNCT_1:18;
y in union C by A1, Th16;
hence {((id (union C)) . x),((id (union C)) . y)} in C by A1, A2, FUNCT_1:18; :: thesis: verum

end;

hence [[C,C],(id (union C))] is Element of MapsC X by Th19; :: thesis: verum