set f = id (union C);

now

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

end;

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