A5: gcd (s1,s2,Amp) = 1. R by A2, Th43;
A6: ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = r1 iff z = (r1 * s2) + (r2 * s1) ) )

proof

assume that
A7: s1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = r1 iff z = (r1 * s2) + (r2 * s1) )
A8: s2 = 1. R by A4, A5, A7, Th30;
let z be Element of R; :: thesis: ( z = r1 iff z = (r1 * s2) + (r2 * s1) )
(r1 * s2) + (r2 * s1) = (r1 * s2) + (0. R) by A7
.= r1 * (1. R) by A8, RLVECT_1:4
.= r1 ;
hence ( z = r1 iff z = (r1 * s2) + (r2 * s1) ) ; :: thesis: verum

end;

A9: ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r1 iff z = 0. R ) )

proof

A10: 1. R <> 0. R ;
assume that
A11: s1 = 0. R and
A12: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = r1 iff z = 0. R )
let z be Element of R; :: thesis: ( z = r1 iff z = 0. R )
A13: s2 = 1. R by A4, A5, A11, Th30;
then A14: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (r1 * (s2 / (gcd (r2,s2,Amp)))) + (0. R) by A11, A12
.= r1 * ((1. R) / (gcd (r2,s2,Amp))) by A13, RLVECT_1:4
.= r1 * (1. R) by A14, A10, Th9
.= r1 ;
hence ( z = r1 iff z = 0. R ) ; :: thesis: verum

end;

A15: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A16: ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = s1 iff z = (r1 * s2) + (r2 * s1) ) )

proof

assume that
A17: r1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = s1 iff z = (r1 * s2) + (r2 * s1) )
A18: r2 = 1. R by A3, A15, A17, Th30;
let z be Element of R; :: thesis: ( z = s1 iff z = (r1 * s2) + (r2 * s1) )
(r1 * s2) + (r2 * s1) = (0. R) + (r2 * s1) by A17
.= (1. R) * s1 by A18, RLVECT_1:4
.= s1 ;
hence ( z = s1 iff z = (r1 * s2) + (r2 * s1) ) ; :: thesis: verum

end;

A19: ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = s1 iff z = 0. R ) )

proof

A20: 1. R <> 0. R ;
assume that
A21: r1 = 0. R and
A22: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = s1 iff z = 0. R )
let z be Element of R; :: thesis: ( z = s1 iff z = 0. R )
A23: r2 = 1. R by A3, A15, A21, Th30;
then A24: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (0. R) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A21, A22
.= s1 * ((1. R) / (gcd (r2,s2,Amp))) by A23, RLVECT_1:4
.= s1 * (1. R) by A24, A20, Th9
.= s1 ;
hence ( z = s1 iff z = 0. R ) ; :: thesis: verum

end;

( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = (r1 * s2) + (r2 * s1) iff z = 0. R ) )

proof

assume A25: ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ) ; :: thesis: for z being Element of R holds
( z = (r1 * s2) + (r2 * s1) iff z = 0. R )
let z be Element of R; :: thesis: ( z = (r1 * s2) + (r2 * s1) iff z = 0. R )
0. R = (r1 * s2) + (s1 * (r2 / (1. R))) by A25, Th10
.= (r1 * s2) + (s1 * r2) by Th10 ;
hence ( z = (r1 * s2) + (r2 * s1) iff z = 0. R ) ; :: thesis: verum

end;

hence for b₁ being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b₁ = s1 iff b₁ = r1 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = s1 iff b₁ = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = s1 iff b₁ = 0. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = r1 iff b₁ = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = r1 iff b₁ = 0. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = (r1 * s2) + (r2 * s1) iff b₁ = 0. R ) ) ) by A16, A19, A6, A9; :: thesis: verum