let i1, i2, i5, i3, i4 be Integer; :: thesis: ( i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies i1 * i3,i2 * i4 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5 ; :: thesis: i1 * i3,i2 * i4 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def3;
consider i9 being Integer such that
A4: i5 * i9 = i3 - i4 by A2, Def3;
(i1 * i3) - (i2 * i4) = ((i1 - i2) * i3) + ((i3 - i4) * i2)
.= ((i5 * i8) * i3) + ((i5 * i9) * i2) by A3, A4
.= i5 * ((i8 * i3) + (i9 * i2)) ;
hence i1 * i3,i2 * i4 are_congruent_mod i5 by Def3; :: thesis: verum