let i1, i2, i3, i4, i5 be Integer; ( 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
; i1 + i3,i2 + i4 are_congruent_mod i5
consider i8 being Integer such that
A3:
i5 * i8 = i1 - i2
by A1;
consider i9 being Integer such that
A4:
i5 * i9 = i3 - i4
by A2;
i5 * (i8 + i9) = (i1 + i3) - (i2 + i4)
by A3, A4;
hence
i1 + i3,i2 + i4 are_congruent_mod i5
; verum