set f = C idval X;
A1: dom (C idval X) = X by ThIV;

hereby :: according to ABCMIZ_1:def 58 :: thesis: C idval X is one-to-one

let x be variable; :: thesis: ( x in dom (C idval X) implies ex y being variable st (C idval X) . x = y -term C )
assume A0: x in dom (C idval X) ; :: thesis: ex y being variable st (C idval X) . x = y -term C
take y = x; :: thesis: (C idval X) . x = y -term C
thus (C idval X) . x = y -term C by A0, A1, ThIV; :: thesis: verum

end;

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom (C idval X) or not y in dom (C idval X) or not (C idval X) . x = (C idval X) . y or x = y )
assume A2: ( x in dom (C idval X) & y in dom (C idval X) ) ; :: thesis: ( not (C idval X) . x = (C idval X) . y or x = y )
then reconsider x = x, y = y as variable ;
( (C idval X) . x = x -term C & (C idval X) . y = y -term C ) by A1, A2, ThIV;
hence ( not (C idval X) . x = (C idval X) . y or x = y ) by ThT0; :: thesis: verum