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 5;
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 5;
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