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 A1: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp ) ; :: thesis: add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
then A2: ( r2 in Amp & s2 in Amp & r2 <> 0. R & s2 <> 0. R ) by Def15;
then A3: ( r2 = NF r2,Amp & s2 = NF s2,Amp & r2 <> 0. R & s2 <> 0. R ) by Def9;
A4: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R ) by A1, Def15;
then A5: ( r1,r2 are_co-prime & s1,s2 are_co-prime ) by Def14;

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 A6: 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 A3, A5, Def17;
hence add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A1, A3, A5, A6, Def16; :: thesis: verum

end;

case A7: 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 A3, A5, Def17;
hence add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A1, A3, A5, A7, Def16; :: thesis: verum

end;

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

then A9: add1 r1,r2,s1,s2,Amp = (r1 * s2) + (r2 * s1) by A3, A5, Def16;
A10: add2 r1,r2,s1,s2,Amp = r2 * s2 by A3, A5, A8, Def17;
then A11: 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 A9, 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 A8, Th10
.= gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp by A2, A4, Th41
.= 1. R by A8, Th33 ;
reconsider r2 = r2, s2 = s2 as Element of Amp by A1, Def15;
A12: r2 * s2 in Amp by A1, Def10;
r2 * s2 <> 0. R by A2, VECTSP_2:def 5;
hence add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A10, A11, A12, Def15; :: thesis: verum

end;

case (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 A13: add2 r1,r2,s1,s2,Amp = 1. R by A3, A5, Def17;
then A14: gcd (add1 r1,r2,s1,s2,Amp),(add2 r1,r2,s1,s2,Amp),Amp = 1. R by Th33;
A15: 1. R in Amp by Th22;
1. R <> 0. R ;
hence add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A13, A14, A15, Def15; :: thesis: verum

end;

case A16: ( 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 A17: 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) by A3, A5, Def16;
A18: 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 A3, A5, A16, Def17;
A19: 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 A2, A4, Th41;
gcd r2,s2,Amp <> 0. R by A2, Th34;
then gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp <> 0. R by Th34;
then A20: 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 A19, Th39;
reconsider r2 = r2, s2 = s2 as Element of Amp by A1, Def15;
A21: gcd r2,s2,Amp divides s2 by Def12;
A22: gcd r2,s2,Amp <> 0. R by A2, Th34;
gcd r2,s2,Amp in Amp by Def12;
then reconsider z3 = s2 / (gcd r2,s2,Amp) as Element of Amp by A1, A21, A22, Th27;
r2 * z3 in Amp by A1, Def10;
then reconsider z1 = r2 * (s2 / (gcd r2,s2,Amp)) as Element of Amp ;
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;
A23: z2 divides z1

proof

A24: z2 divides gcd r2,s2,Amp by Def12;
gcd r2,s2,Amp divides r2 by Def12;
then z2 divides r2 by A24, Th2;
hence z2 divides z1 by Th7; :: thesis: verum

end;

A25: z2 <> 0. R by A22, Th34;
then A26: z1 / z2 in Amp by A1, A23, Th27;
z1 / z2 <> 0. R

proof

A27: r2 * s2 <> 0. R by A2, VECTSP_2:def 5;
A28: gcd r2,s2,Amp divides r2 * s2 by A21, Th7;
then z1 = (r2 * s2) / (gcd r2,s2,Amp) by A21, A22, Th11;
then z1 <> 0. R by A22, A27, A28, Th8;
hence z1 / z2 <> 0. R by A23, A25, Th8; :: thesis: verum

end;

hence add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp by A17, A18, A20, A26, 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