let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
let r1, r2, s1, s2 be Element of R; :: thesis: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp )
assume A1: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
then A2: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & s2 in Amp & r2 in Amp ) by Def15;
then A3: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 <> 0. R & s2 <> 0. R & r2 = NF r2,Amp & s2 = NF s2,Amp ) by A1, Def9, Def14, Def15;
then A4: ( gcd r1,s2,Amp <> 0. R & gcd s1,r2,Amp <> 0. R ) by Th34;

now

per cases ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ) ;

case ( r1 = 0. R or s1 = 0. R ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

then A5: mult2 r1,r2,s1,s2,Amp = 1. R by A3, Def19;
then A6: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by Th33;
A7: 1. R in Amp by Th22;
1. R <> 0. R ;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A5, A6, A7, Def15; :: thesis: verum

end;

case ( r2 = 1. R & s2 = 1. R ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

then A8: mult2 r1,r2,s1,s2,Amp = 1. R by A3, Def19;
then A9: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by Th33;
A10: 1. R in Amp by Th22;
1. R <> 0. R ;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A8, A9, A10, Def15; :: thesis: verum

end;

case A11: ( s2 <> 0. R & r2 = 1. R ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

then A12: mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd r1,s2,Amp) by Def18;
A13: mult2 r1,r2,s1,s2,Amp = s2 / (gcd r1,s2,Amp) by A3, A11, Def19;
A14: gcd s1,r2,Amp = 1. R by A11, Th33;
then A15: r2 / (gcd s1,r2,Amp) = 1. R by A11, Th9;
A16: gcd r1,s2,Amp divides r1 by Def12;
then gcd r1,s2,Amp divides r1 * s1 by Th7;
then A17: (r1 * s1) / (gcd r1,s2,Amp) = (r1 / (gcd r1,s2,Amp)) * s1 by A4, A16, Th11
.= (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by A14, Th10 ;
s2 / (gcd r1,s2,Amp) = (s2 / (gcd r1,s2,Amp)) * (r2 / (gcd s1,r2,Amp)) by A15, VECTSP_1:def 13;
then A18: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A2, A3, A12, A13, A17, Th42;
A19: gcd r1,s2,Amp divides s2 by Def12;
A20: gcd r1,s2,Amp <> 0. R by A3, Th34;
then A21: s2 / (gcd r1,s2,Amp) <> 0. R by A3, A19, Th8;
reconsider zz = gcd r1,s2,Amp as Element of Amp by Def12;
reconsider s2 = s2 as Element of Amp by A1, Def15;
s2 / zz in Amp by A1, A19, A20, Th27;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A13, A18, A21, Def15; :: thesis: verum

end;

case A22: ( r2 <> 0. R & s2 = 1. R ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

then A23: mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd s1,r2,Amp) by Def18;
A24: mult2 r1,r2,s1,s2,Amp = r2 / (gcd s1,r2,Amp) by A3, A22, Def19;
A25: gcd r1,s2,Amp = 1. R by A22, Th33;
then A26: s2 / (gcd r1,s2,Amp) = 1. R by A22, Th9;
A27: gcd s1,r2,Amp divides s1 by Def12;
then gcd s1,r2,Amp divides r1 * s1 by Th7;
then A28: (r1 * s1) / (gcd s1,r2,Amp) = r1 * (s1 / (gcd s1,r2,Amp)) by A4, A27, Th11
.= (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by A25, Th10 ;
r2 / (gcd s1,r2,Amp) = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) by A26, VECTSP_1:def 13;
then A29: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A2, A3, A23, A24, A28, Th42;
A30: gcd s1,r2,Amp divides r2 by Def12;
A31: gcd s1,r2,Amp <> 0. R by A3, Th34;
then A32: r2 / (gcd s1,r2,Amp) <> 0. R by A3, A30, Th8;
reconsider zz = gcd s1,r2,Amp as Element of Amp by Def12;
reconsider r2 = r2 as Element of Amp by A1, Def15;
r2 / zz in Amp by A1, A30, A31, Th27;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A24, A29, A32, Def15; :: thesis: verum

end;

case A33: ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

then A34: mult1 r1,r2,s1,s2,Amp = (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by Def18;
A35: mult2 r1,r2,s1,s2,Amp = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) by A3, A33, Def19;
then A36: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A2, A3, A34, Th42;
A37: gcd r1,s2,Amp divides s2 by Def12;
A38: gcd r1,s2,Amp <> 0. R by A3, Th34;
then A39: s2 / (gcd r1,s2,Amp) <> 0. R by A3, A37, Th8;
reconsider z1 = gcd r1,s2,Amp as Element of Amp by Def12;
reconsider s2 = s2 as Element of Amp by A1, Def15;
A40: gcd s1,r2,Amp divides r2 by Def12;
A41: gcd s1,r2,Amp <> 0. R by A3, Th34;
then A42: r2 / (gcd s1,r2,Amp) <> 0. R by A3, A40, Th8;
reconsider z2 = gcd s1,r2,Amp as Element of Amp by Def12;
reconsider r2 = r2 as Element of Amp by A1, Def15;
reconsider u = s2 / z1 as Element of Amp by A1, A37, A38, Th27;
reconsider v = r2 / z2 as Element of Amp by A1, A40, A41, Th27;
A43: v * u in Amp by A1, Def10;
v * u <> 0. R by A39, A42, VECTSP_2:def 5;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A35, A36, A43, Def15; :: thesis: verum

end;

end;

end;

hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp ; :: thesis: verum