let m, a, x, b be Integer; :: thesis: ( m <> 0 & ((a * x) - b) mod m = 0 implies for y being Integer holds
( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class (Cong m),x ) & ( y in Class (Cong m),x implies ((a * y) - b) mod m = 0 ) ) )
assume that
A1: m <> 0 and
A2: ((a * x) - b) mod m = 0 ; :: thesis: for y being Integer holds
( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class (Cong m),x ) & ( y in Class (Cong m),x implies ((a * y) - b) mod m = 0 ) )
let y be Integer; :: thesis: ( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class (Cong m),x ) & ( y in Class (Cong m),x implies ((a * y) - b) mod m = 0 ) )

hereby :: thesis: ( y in Class (Cong m),x implies ((a * y) - b) mod m = 0 )

assume that
A3: a,m are_relative_prime and
A4: ((a * y) - b) mod m = 0 ; :: thesis: y in Class (Cong m),x
(a * x) - b,(a * y) - b are_congruent_mod m by A1, A2, A4, INT_3:12;
then ((a * x) - b) + b,a * y are_congruent_mod m by INT_1:40;
then x,y are_congruent_mod m by A3, Th9;
then [x,y] in Cong m by Def1;
hence y in Class (Cong m),x by EQREL_1:26; :: thesis: verum

end;

assume y in Class (Cong m),x ; :: thesis: ((a * y) - b) mod m = 0
then [x,y] in Cong m by EQREL_1:26;
then x,y are_congruent_mod m by Def1;
then A5: x * a,y * a are_congruent_mod m by Th11;
((a * x) - b) mod m = 0 mod m by A2, Th12;
then 0 ,(a * x) - b are_congruent_mod m by A1, INT_3:12;
then 0 + b,a * x are_congruent_mod m by INT_1:40;
then 0 + b,a * y are_congruent_mod m by A5, INT_1:36;
then 0 ,(a * y) - b are_congruent_mod m by INT_1:40;
then ((a * y) - b) mod m = 0 mod m by INT_3:12;
hence ((a * y) - b) mod m = 0 by Th12; :: thesis: verum