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

proof

set d = (r1 * s1) / (gcd (s1,r2,Amp));
assume that
A2: ( r1 = 0. R or s1 = 0. R ) and
A3: r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
A4: gcd (s1,r2,Amp) <> 0. R by A3, Th33;
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
A5: r1 * s1 = 0. R

proof

now :: thesis: ( ( r1 = 0. R & r1 * s1 = 0. R ) or ( s1 = 0. R & r1 * s1 = 0. R ) )

per cases ( r1 = 0. R or s1 = 0. R ) by A2;

case r1 = 0. R ; :: thesis: r1 * s1 = 0. R

hence r1 * s1 = 0. R ; :: thesis: verum

end;

case s1 = 0. R ; :: thesis: r1 * s1 = 0. R

hence r1 * s1 = 0. R ; :: thesis: verum

end;

end;

end;

hence r1 * s1 = 0. R ; :: thesis: verum

end;

gcd (s1,r2,Amp) divides s1 by Def12;
then gcd (s1,r2,Amp) divides r1 * s1 by Th7;
then ((r1 * s1) / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = 0. R by A5, A4, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) by A4, VECTSP_2:def 1; :: thesis: verum

end;

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

proof

set d = (r1 * s1) / (gcd (r1,s2,Amp));
assume that
A7: ( r1 = 0. R or s1 = 0. R ) and
A8: s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
A9: gcd (r1,s2,Amp) <> 0. R by A8, Th33;
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
A10: r1 * s1 = 0. R

proof

now :: thesis: ( ( r1 = 0. R & r1 * s1 = 0. R ) or ( s1 = 0. R & r1 * s1 = 0. R ) )

per cases ( r1 = 0. R or s1 = 0. R ) by A7;

case r1 = 0. R ; :: thesis: r1 * s1 = 0. R

hence r1 * s1 = 0. R ; :: thesis: verum

end;

case s1 = 0. R ; :: thesis: r1 * s1 = 0. R

hence r1 * s1 = 0. R ; :: thesis: verum

end;

end;

end;

hence r1 * s1 = 0. R ; :: thesis: verum

end;

gcd (r1,s2,Amp) divides r1 by Def12;
then gcd (r1,s2,Amp) divides r1 * s1 by Th7;
then ((r1 * s1) / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = 0. R by A10, A9, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) by A9, VECTSP_2:def 1; :: thesis: verum

end;

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

proof

assume that
A12: r2 = 1. R and
s2 = 1. R and
r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
gcd (s1,r2,Amp) = 1. R by A12, Th32;
hence for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) by Th10; :: thesis: verum

end;

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

proof

assume that
r2 = 1. R and
A13: s2 = 1. R and
s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
gcd (r1,s2,Amp) = 1. R by A13, Th32;
hence for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) by Th10; :: thesis: verum

end;

hence for b₁ being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) ) by A6, A1, A11; :: thesis: verum