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
add1 (r1,r2,s1,s2,Amp), add2 (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
add1 (r1,r2,s1,s2,Amp), add2 (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 add1 (r1,r2,s1,s2,Amp), add2 (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: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A4: r2 <> 0. R by A2, Def15;
r2 in Amp by A2, Def15;
then A5: r2 = NF (r2,Amp) by Def9;
s2 in Amp by A3, Def15;
then A6: s2 = NF (s2,Amp) by Def9;
A7: gcd (r1,r2,Amp) = 1. R by A2, Def15;
then A8: r1,r2 are_co-prime by Def14;
A9: gcd (s1,s2,Amp) = 1. R by A3, Def15;
then A10: s1,s2 are_co-prime by Def14;
A11: s2 <> 0. R by A3, Def15;

now

per cases ( r1 = 0. R or s1 = 0. R or gcd (r2,s2,Amp) = 1. R or (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R or ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ) ;

case A12: r1 = 0. R ; :: thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp

then add2 (r1,r2,s1,s2,Amp) = s2 by A5, A6, A8, A10, Def17;
hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A3, A5, A6, A8, A10, A12, Def16; :: thesis: verum

end;

case A13: s1 = 0. R ; :: thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp

then add2 (r1,r2,s1,s2,Amp) = r2 by A5, A6, A8, A10, Def17;
hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A2, A5, A6, A8, A10, A13, Def16; :: thesis: verum

end;

case A14: gcd (r2,s2,Amp) = 1. R ; :: thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp

then A15: add2 (r1,r2,s1,s2,Amp) = r2 * s2 by A5, A6, A8, A10, Def17;
add1 (r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) by A5, A6, A8, A10, A14, Def16;
then A16: gcd ((add1 (r1,r2,s1,s2,Amp)),(add2 (r1,r2,s1,s2,Amp)),Amp) = gcd (((r1 * (s2 / (1. R))) + (s1 * r2)),(r2 * s2),Amp) by A15, Th10
.= gcd (((r1 * (s2 / (1. R))) + (s1 * (r2 / (1. R)))),(r2 * s2),Amp) by Th10
.= gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(r2 * (s2 / (gcd (r2,s2,Amp)))),Amp) by A14, Th10
.= gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) by A4, A7, A9, Th41
.= 1. R by A14, Th33 ;
reconsider r2 = r2, s2 = s2 as Element of Amp by A2, A3, Def15;
( r2 * s2 in Amp & r2 * s2 <> 0. R ) by A1, A4, A11, Def10, VECTSP_2:def 1;
hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A15, A16, Def15; :: thesis: verum

end;

case A17: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; :: thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp

A18: ( 1. R in Amp & 1. R <> 0. R ) by Th22;
A19: add2 (r1,r2,s1,s2,Amp) = 1. R by A5, A6, A8, A10, A17, Def17;
then gcd ((add1 (r1,r2,s1,s2,Amp)),(add2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by Th33;
hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A19, A18, Def15; :: thesis: verum

end;

case ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ; :: thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp

then A20: ( add1 (r1,r2,s1,s2,Amp) = ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) & add2 (r1,r2,s1,s2,Amp) = (r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) ) by A5, A6, A8, A10, Def16, Def17;
gcd (r2,s2,Amp) <> 0. R by A4, Th34;
then A21: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) <> 0. R by Th34;
gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(r2 * (s2 / (gcd (r2,s2,Amp)))),Amp) = gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) by A4, A7, A9, Th41;
then A22: gcd ((((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp))),((r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp))),Amp) = 1. R by A21, Th39;
reconsider r2 = r2, s2 = s2 as Element of Amp by A2, A3, Def15;
A23: gcd (r2,s2,Amp) divides s2 by Def12;
reconsider z2 = gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) as Element of Amp by Def12;
A24: gcd (r2,s2,Amp) <> 0. R by A4, Th34;
then A25: z2 <> 0. R by Th34;
gcd (r2,s2,Amp) in Amp by Def12;
then reconsider z3 = s2 / (gcd (r2,s2,Amp)) as Element of Amp by A1, A23, A24, Th27;
r2 * z3 in Amp by A1, Def10;
then reconsider z1 = r2 * (s2 / (gcd (r2,s2,Amp))) as Element of Amp ;
A26: r2 * s2 <> 0. R by A4, A11, VECTSP_2:def 1;
A27: gcd (r2,s2,Amp) divides r2 * s2 by A23, Th7;
then z1 = (r2 * s2) / (gcd (r2,s2,Amp)) by A23, A24, Th11;
then A28: z1 <> 0. R by A24, A26, A27, Th8;
( z2 divides gcd (r2,s2,Amp) & gcd (r2,s2,Amp) divides r2 ) by Def12;
then A29: z2 divides r2 by Th2;
then z2 divides z1 by Th7;
then A30: z1 / z2 <> 0. R by A25, A28, Th8;
z1 / z2 in Amp by A1, A29, A25, Th7, Th27;
hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A20, A22, A30, Def15; :: thesis: verum

end;

end;

end;

hence add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ; :: thesis: verum