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 that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
A4: gcd r1,r2,Amp = 1. R by A2, Def15;
then A5: r1,r2 are_co-prime by Def14;
s2 in Amp by A3, Def15;
then A6: s2 = NF s2,Amp by Def9;
r2 in Amp by A2, Def15;
then A7: r2 = NF r2,Amp by Def9;
A8: r2 <> 0. R by A2, Def15;
then A9: gcd s1,r2,Amp <> 0. R by Th34;
A10: gcd s1,s2,Amp = 1. R by A3, Def15;
then A11: s1,s2 are_co-prime by Def14;
A12: s2 <> 0. R by A3, Def15;
then A13: gcd r1,s2,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 A14: ( r1 = 0. R or s1 = 0. R ) ; :: thesis: mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp

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

end;

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

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

end;

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

then A21: gcd s1,r2,Amp = 1. R by Th33;
then r2 / (gcd s1,r2,Amp) = 1. R by A20, Th9;
then A22: s2 / (gcd r1,s2,Amp) = (s2 / (gcd r1,s2,Amp)) * (r2 / (gcd s1,r2,Amp)) by VECTSP_1:def 13;
A23: gcd r1,s2,Amp divides r1 by Def12;
then gcd r1,s2,Amp divides r1 * s1 by Th7;
then A24: (r1 * s1) / (gcd r1,s2,Amp) = (r1 / (gcd r1,s2,Amp)) * s1 by A13, A23, Th11
.= (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by A21, Th10 ;
A25: mult2 r1,r2,s1,s2,Amp = s2 / (gcd r1,s2,Amp) by A5, A11, A7, A6, A20, Def19;
reconsider zz = gcd r1,s2,Amp as Element of Amp by Def12;
A26: ( gcd r1,s2,Amp divides s2 & gcd r1,s2,Amp <> 0. R ) by A12, Def12, Th34;
then A27: s2 / (gcd r1,s2,Amp) <> 0. R by A12, Th8;
mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd r1,s2,Amp) by A20, Def18;
then A28: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A4, A10, A8, A12, A25, A24, A22, Th42;
reconsider s2 = s2 as Element of Amp by A3, Def15;
s2 / zz in Amp by A1, A26, Th27;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A25, A28, A27, Def15; :: thesis: verum

end;

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

then A30: gcd r1,s2,Amp = 1. R by Th33;
then s2 / (gcd r1,s2,Amp) = 1. R by A29, Th9;
then A31: r2 / (gcd s1,r2,Amp) = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) by VECTSP_1:def 13;
A32: gcd s1,r2,Amp divides s1 by Def12;
then gcd s1,r2,Amp divides r1 * s1 by Th7;
then A33: (r1 * s1) / (gcd s1,r2,Amp) = r1 * (s1 / (gcd s1,r2,Amp)) by A9, A32, Th11
.= (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by A30, Th10 ;
A34: mult2 r1,r2,s1,s2,Amp = r2 / (gcd s1,r2,Amp) by A5, A11, A7, A6, A29, Def19;
reconsider zz = gcd s1,r2,Amp as Element of Amp by Def12;
A35: ( gcd s1,r2,Amp divides r2 & gcd s1,r2,Amp <> 0. R ) by A8, Def12, Th34;
then A36: r2 / (gcd s1,r2,Amp) <> 0. R by A8, Th8;
mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd s1,r2,Amp) by A29, Def18;
then A37: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A4, A10, A8, A12, A34, A33, A31, Th42;
reconsider r2 = r2 as Element of Amp by A2, Def15;
r2 / zz in Amp by A1, A35, Th27;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A34, A37, A36, Def15; :: thesis: verum

end;

case A38: ( 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

reconsider z2 = gcd s1,r2,Amp as Element of Amp by Def12;
reconsider z1 = gcd r1,s2,Amp as Element of Amp by Def12;
A39: ( gcd r1,s2,Amp divides s2 & gcd r1,s2,Amp <> 0. R ) by A12, Def12, Th34;
then A40: s2 / (gcd r1,s2,Amp) <> 0. R by A12, Th8;
A41: mult2 r1,r2,s1,s2,Amp = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) by A5, A11, A7, A6, A38, Def19;
mult1 r1,r2,s1,s2,Amp = (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) by A38, Def18;
then A42: gcd (mult1 r1,r2,s1,s2,Amp),(mult2 r1,r2,s1,s2,Amp),Amp = 1. R by A4, A10, A8, A12, A41, Th42;
A43: ( gcd s1,r2,Amp divides r2 & gcd s1,r2,Amp <> 0. R ) by A8, Def12, Th34;
then A44: r2 / (gcd s1,r2,Amp) <> 0. R by A8, Th8;
reconsider s2 = s2 as Element of Amp by A3, Def15;
reconsider u = s2 / z1 as Element of Amp by A1, A39, Th27;
reconsider r2 = r2 as Element of Amp by A2, Def15;
reconsider v = r2 / z2 as Element of Amp by A1, A43, Th27;
A45: v * u <> 0. R by A40, A44, VECTSP_2:def 5;
v * u in Amp by A1, Def10;
hence mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A41, A42, A45, 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