A2: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R ) by A1, Th44;
A3: ( 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 A4: ( r1 = 0. R & gcd r2,s2,Amp = 1. R ) ; :: thesis: for z being Element of R holds
( z = s1 iff z = (r1 * s2) + (r2 * s1) )
let z be Element of R; :: thesis: ( z = s1 iff z = (r1 * s2) + (r2 * s1) )
A5: r2 = 1. R by A1, A2, A4, Th31;
(r1 * s2) + (r2 * s1) = (0. R) + (r2 * s1) by A4, VECTSP_1:39
.= (1. R) * s1 by A5, RLVECT_1:10
.= s1 by VECTSP_1:def 19 ;
hence ( z = s1 iff z = (r1 * s2) + (r2 * s1) ) ; :: thesis: verum

end;

A6: ( 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

assume A7: ( r1 = 0. R & (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 )
A8: r2 = 1. R by A1, A2, A7, Th31;
then A9: gcd r2,s2,Amp = 1. R by Th33;
A10: 1. R <> 0. R ;
0. R = (0. R) + (s1 * (r2 / (gcd r2,s2,Amp))) by A7, VECTSP_1:39
.= s1 * ((1. R) / (gcd r2,s2,Amp)) by A8, RLVECT_1:10
.= s1 * (1. R) by A9, A10, Th9
.= s1 by VECTSP_1:def 13 ;
hence ( z = s1 iff z = 0. R ) ; :: thesis: verum

end;

A11: ( 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 A12: ( s1 = 0. R & gcd r2,s2,Amp = 1. R ) ; :: thesis: for z being Element of R holds
( z = r1 iff z = (r1 * s2) + (r2 * s1) )
let z be Element of R; :: thesis: ( z = r1 iff z = (r1 * s2) + (r2 * s1) )
A13: s2 = 1. R by A1, A2, A12, Th31;
(r1 * s2) + (r2 * s1) = (r1 * s2) + (0. R) by A12, VECTSP_1:39
.= r1 * (1. R) by A13, RLVECT_1:10
.= r1 by VECTSP_1:def 13 ;
hence ( z = r1 iff z = (r1 * s2) + (r2 * s1) ) ; :: thesis: verum

end;

A14: ( 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

assume A15: ( s1 = 0. 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 iff z = 0. R )
let z be Element of R; :: thesis: ( z = r1 iff z = 0. R )
A16: s2 = 1. R by A1, A2, A15, Th31;
then A17: gcd r2,s2,Amp = 1. R by Th33;
A18: 1. R <> 0. R ;
0. R = (r1 * (s2 / (gcd r2,s2,Amp))) + (0. R) by A15, VECTSP_1:39
.= r1 * ((1. R) / (gcd r2,s2,Amp)) by A16, RLVECT_1:10
.= r1 * (1. R) by A17, A18, Th9
.= r1 by VECTSP_1:def 13 ;
hence ( z = r1 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 A19: ( 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 A19, 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 A3, A6, A11, A14; :: thesis: verum