set I = id INT;
set f = i (#) (id INT);
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (i (#) (id INT)) or not x2 in proj1 (i (#) (id INT)) or not (i (#) (id INT)) . x1 = (i (#) (id INT)) . x2 or x1 = x2 )
assume ( x1 in dom (i (#) (id INT)) & x2 in dom (i (#) (id INT)) ) ; :: thesis: ( not (i (#) (id INT)) . x1 = (i (#) (id INT)) . x2 or x1 = x2 )
then reconsider x1 = x1, x2 = x2 as Element of INT ;
( (i (#) (id INT)) . x1 = i * ((id INT) . x1) & (i (#) (id INT)) . x2 = i * ((id INT) . x2) ) by VALUED_1:6;
hence ( not (i (#) (id INT)) . x1 = (i (#) (id INT)) . x2 or x1 = x2 ) by XCMPLX_1:5; :: thesis: verum