A5: gcd s1,s2,Amp = 1. R by A2, Th44;
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, Th31;
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, VECTSP_1:39
.= r1 * (1. R) by A8, RLVECT_1:10
.= r1 by VECTSP_1:def 13 ;
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, Th31;
then A14: gcd r2,s2,Amp = 1. R by Th33;
0. R = (r1 * (s2 / (gcd r2,s2,Amp))) + (0. R) by A11, A12, VECTSP_1:39
.= r1 * ((1. R) / (gcd r2,s2,Amp)) by A13, RLVECT_1:10
.= r1 * (1. R) by A14, A10, Th9
.= r1 by VECTSP_1:def 13 ;
hence ( z = r1 iff z = 0. R ) ; :: 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 = 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, Th31;
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, VECTSP_1:39
.= (1. R) * s1 by A18, RLVECT_1:10
.= s1 by VECTSP_1:def 19 ;
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, Th31;
then A24: gcd r2,s2,Amp = 1. R by Th33;
0. R = (0. R) + (s1 * (r2 / (gcd r2,s2,Amp))) by A21, A22, VECTSP_1:39
.= s1 * ((1. R) / (gcd r2,s2,Amp)) by A23, RLVECT_1:10
.= s1 * (1. R) by A24, A20, Th9
.= s1 by VECTSP_1:def 13 ;
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