let i be non zero Integer; :: thesis: INT , multiples i are_equipotent
set M = multiples i;
set I = id INT;
set f = i (#) (id INT);
take i (#) (id INT) ; :: according to WELLORD2:def 4 :: thesis: ( i (#) (id INT) is one-to-one & proj1 (i (#) (id INT)) = INT & proj2 (i (#) (id INT)) = multiples i )
thus i (#) (id INT) is one-to-one ; :: thesis: ( proj1 (i (#) (id INT)) = INT & proj2 (i (#) (id INT)) = multiples i )
thus dom (i (#) (id INT)) = INT by VALUED_1:def 5; :: thesis: proj2 (i (#) (id INT)) = multiples i
thus rng (i (#) (id INT)) = multiples i :: thesis: verum

proof

thus rng (i (#) (id INT)) c= multiples i :: according to XBOOLE_0:def 10 :: thesis: multiples i c= rng (i (#) (id INT))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (i (#) (id INT)) or y in multiples i )
assume y in rng (i (#) (id INT)) ; :: thesis: y in multiples i
then consider x being object such that
x in dom (i (#) (id INT)) and
A1: (i (#) (id INT)) . x = y by FUNCT_1:def 3;
reconsider y = y as Integer by A1;
(i (#) (id INT)) . x = i * ((id INT) . x) by VALUED_1:6;
then i divides y by A1;
then y is Multiple of i by Def15;
hence y in multiples i ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in multiples i or y in rng (i (#) (id INT)) )
assume y in multiples i ; :: thesis: y in rng (i (#) (id INT))
then reconsider m = y as Multiple of i by Th61;
i divides m by Def15;
then consider j being Integer such that
A2: m = i * j ;
reconsider j = j as Element of INT by INT_1:def 2;
A3: dom (i (#) (id INT)) = INT by VALUED_1:def 5;
(i (#) (id INT)) . j = i * ((id INT) . j) by VALUED_1:6
.= y by A2 ;
hence y in rng (i (#) (id INT)) by A3, FUNCT_1:def 3; :: thesis: verum

end;