A5: ( 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 = r2 * s2 iff z = 1. R ) )

proof

assume that
A6: gcd (r2,s2,Amp) = 1. R and
A7: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = r2 * s2 iff z = 1. R )
A8: 0. R = (r1 * s2) + (s1 * (r2 / (1. R))) by A6, A7, Th10
.= (r1 * s2) + (s1 * r2) by Th10 ;
then A9: r1 * s2 = - (s1 * r2) by RLVECT_1:19;
A10: s1 * r2 = - (r1 * s2) by A8, RLVECT_1:19;
gcd (s2,s1,Amp) = 1. R by A2, Th44;
then gcd (s2,(s1 * r2),Amp) = gcd (s2,r2,Amp) by Th38
.= 1. R by A6, Th30 ;
then 1. R = gcd (((1. R) * s2),(- (r1 * s2)),Amp) by A10, VECTSP_1:def 19
.= gcd (((1. R) * s2),((- r1) * s2),Amp) by VECTSP_1:40 ;
then A11: 1. R is_associated_to s2 * (gcd ((1. R),(- r1),Amp)) by Th37;
let z be Element of R; :: thesis: ( z = r2 * s2 iff z = 1. R )
A12: 1. R in Amp by Th22;
gcd (r2,r1,Amp) = 1. R by A1, Th44;
then gcd (r2,(r1 * s2),Amp) = 1. R by A6, Th38;
then 1. R = gcd (((1. R) * r2),(- (s1 * r2)),Amp) by A9, VECTSP_1:def 19
.= gcd (((1. R) * r2),((- s1) * r2),Amp) by VECTSP_1:40 ;
then A13: 1. R is_associated_to r2 * (gcd ((1. R),(- s1),Amp)) by Th37;
s2 * (gcd ((1. R),(- r1),Amp)) = s2 * (1. R) by Th33
.= s2 by VECTSP_1:def 13 ;
then A14: s2 = 1. R by A4, A12, A11, Def9;
r2 * (gcd ((1. R),(- s1),Amp)) = r2 * (1. R) by Th33
.= r2 by VECTSP_1:def 13 ;
then r2 = 1. R by A3, A13, A12, Def9;
hence ( z = r2 * s2 iff z = 1. R ) by A14, VECTSP_1:def 13; :: thesis: verum

end;

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

proof

assume that
A17: r1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = r2 * s2 )
let z be Element of R; :: thesis: ( z = s2 iff z = r2 * s2 )
r2 = 1. R by A3, A15, A17, Th31;
hence ( z = s2 iff z = r2 * s2 ) by VECTSP_1:def 19; :: thesis: verum

end;

A18: gcd (s1,s2,Amp) = 1. R by A2, Th44;
A19: ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = r2 iff z = r2 * s2 ) )

proof

assume that
A20: s1 = 0. R and
gcd (r2,s2,Amp) = 1. R ; :: thesis: for z being Element of R holds
( z = r2 iff z = r2 * s2 )
let z be Element of R; :: thesis: ( z = r2 iff z = r2 * s2 )
s2 = 1. R by A4, A18, A20, Th31;
hence ( z = r2 iff z = r2 * s2 ) by VECTSP_1:def 13; :: thesis: verum

end;

A21: ( 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 = r2 iff z = 1. R ) )

proof

A22: 1. R <> 0. R ;
assume that
A23: s1 = 0. R and
A24: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = r2 iff z = 1. R )
let z be Element of R; :: thesis: ( z = r2 iff z = 1. R )
A25: s2 = 1. R by A4, A18, A23, Th31;
then A26: gcd (r2,s2,Amp) = 1. R by Th33;
0. R = (r1 * (s2 / (gcd (r2,s2,Amp)))) + (0. R) by A23, A24, VECTSP_1:39
.= r1 * ((1. R) / (gcd (r2,s2,Amp))) by A25, RLVECT_1:10
.= r1 * (1. R) by A26, A22, Th9
.= r1 by VECTSP_1:def 13 ;
hence ( z = r2 iff z = 1. R ) by A3, A15, Th31; :: thesis: verum

end;

A27: ( 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 = s2 iff z = 1. R ) )

proof

A28: 1. R <> 0. R ;
assume that
A29: r1 = 0. R and
A30: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = 1. R )
let z be Element of R; :: thesis: ( z = s2 iff z = 1. R )
A31: r2 = 1. R by A3, A15, A29, Th31;
then A32: gcd (r2,s2,Amp) = 1. R by Th33;
0. R = (0. R) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A29, A30, VECTSP_1:39
.= s1 * ((1. R) / (gcd (r2,s2,Amp))) by A31, RLVECT_1:10
.= s1 * (1. R) by A32, A28, Th9
.= s1 by VECTSP_1:def 13 ;
hence ( z = s2 iff z = 1. R ) by A4, A18, Th31; :: thesis: verum

end;

( r1 = 0. R & s1 = 0. R implies for z being Element of R holds
( z = s2 iff z = r2 ) )

proof

assume that
A33: r1 = 0. R and
A34: s1 = 0. R ; :: thesis: for z being Element of R holds
( z = s2 iff z = r2 )
let z be Element of R; :: thesis: ( z = s2 iff z = r2 )
r2 = 1. R by A3, A15, A33, Th31;
hence ( z = s2 iff z = r2 ) by A4, A18, A34, Th31; :: thesis: verum

end;

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