set f = C idval X;
A1: dom (C idval X) = X by Th131;
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 A2: 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 A1, A2, Th131; :: thesis: verum
end;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 (C idval X) or not y in proj1 (C idval X) or not (C idval X) . x = (C idval X) . y or x = y )
assume that
A3: x in dom (C idval X) and
A4: y in dom (C idval X) ; :: thesis: ( not (C idval X) . x = (C idval X) . y or x = y )
reconsider x = x, y = y as variable by A3, A4;
A5: (C idval X) . x = x -term C by A1, A3, Th131;
(C idval X) . y = y -term C by A1, A4, Th131;
hence ( not (C idval X) . x = (C idval X) . y or x = y ) by A5, Th50; :: thesis: verum