let i1, i2 be Element of INT.Ring; :: thesis: ( i1,i2 are_coprime implies ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1 )
assume A1: i1,i2 are_coprime ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
reconsider ii1 = i1, ii2 = i2 as Integer ;
consider j1, j2 being Element of INT.Ring such that
T1: (ii1 * j1) + (ii2 * j2) = 1 by LmGCD1, A1;
(i1 * j1) + (i2 * j2) = 1 by T1;
hence ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1 ; :: thesis: verum