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, NAT_D:64;
then ((a * x) - b) + b,a * y are_congruent_mod m by INT_1:19;
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:18; :: 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:18;
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, NAT_D:64;
then 0 + b,a * x are_congruent_mod m by INT_1:19;
then 0 + b,a * y are_congruent_mod m by A5, INT_1:15;
then 0 ,(a * y) - b are_congruent_mod m by INT_1:19;
then ((a * y) - b) mod m = 0 mod m by NAT_D:64;
hence ((a * y) - b) mod m = 0 by Th12; :: thesis: verum