let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
let r1, r2, s1, s2 be Element of R; :: thesis: ( r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) )
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp ; :: thesis: (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
gcd r1,r2,Amp = 1. R by A1, Def15;
then A3: r1,r2 are_co-prime by Def14;
s2 in Amp by A2, Def15;
then A4: s2 = NF s2,Amp by Def9;
gcd s1,s2,Amp = 1. R by A2, Def15;
then A5: s1,s2 are_co-prime by Def14;
r2 in Amp by A1, Def15;
then A6: r2 = NF r2,Amp by Def9;
A7: r2 <> 0. R by A1, 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 A8: r1 = 0. R ; :: thesis: (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))

then A9: add1 r1,r2,s1,s2,Amp = s1 by A3, A5, A6, A4, Def16;
add2 r1,r2,s1,s2,Amp = s2 by A3, A5, A6, A4, A8, Def17;
then (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = s2 * ((0. R) + (s1 * r2)) by A8, VECTSP_1:39
.= s2 * (s1 * r2) by RLVECT_1:10
.= (add1 r1,r2,s1,s2,Amp) * (r2 * s2) by A9, GROUP_1:def 4 ;
hence (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum

end;

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

then A11: add1 r1,r2,s1,s2,Amp = r1 by A3, A5, A6, A4, Def16;
add2 r1,r2,s1,s2,Amp = r2 by A3, A5, A6, A4, A10, Def17;
then (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = r2 * ((r1 * s2) + (0. R)) by A10, VECTSP_1:39
.= r2 * (r1 * s2) by RLVECT_1:10
.= (add1 r1,r2,s1,s2,Amp) * (r2 * s2) by A11, GROUP_1:def 4 ;
hence (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum

end;

case A12: gcd r2,s2,Amp = 1. R ; :: thesis: (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))

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

end;

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

A14: (r1 * s2) + (s1 * r2) = 0. R

proof

A15: gcd r2,s2,Amp divides r2 by Def12;
then A16: gcd r2,s2,Amp divides s1 * r2 by Th7;
A17: gcd r2,s2,Amp divides s2 by Def12;
then consider f being Element of R such that
A18: (gcd r2,s2,Amp) * f = s2 by Def1;
A19: gcd r2,s2,Amp <> 0. R by A7, Th34;
consider e being Element of R such that
A20: (gcd r2,s2,Amp) * e = r2 by A15, Def1;
(gcd r2,s2,Amp) * ((e * s1) + (f * r1)) = ((gcd r2,s2,Amp) * (e * s1)) + ((gcd r2,s2,Amp) * (f * r1)) by VECTSP_1:def 11
.= (((gcd r2,s2,Amp) * e) * s1) + ((gcd r2,s2,Amp) * (f * r1)) by GROUP_1:def 4
.= (r1 * s2) + (s1 * r2) by A20, A18, GROUP_1:def 4 ;
then A21: gcd r2,s2,Amp divides (r1 * s2) + (s1 * r2) by Def1;
A22: gcd r2,s2,Amp divides r1 * s2 by A17, Th7;
then 0. R = ((r1 * s2) / (gcd r2,s2,Amp)) + (s1 * (r2 / (gcd r2,s2,Amp))) by A13, A19, A17, Th11
.= ((r1 * s2) / (gcd r2,s2,Amp)) + ((s1 * r2) / (gcd r2,s2,Amp)) by A19, A15, A16, Th11 ;
then A23: 0. R = ((r1 * s2) + (s1 * r2)) / (gcd r2,s2,Amp) by A19, A22, A16, A21, Th12;
0. R = (0. R) * (gcd r2,s2,Amp) by VECTSP_1:39
.= (r1 * s2) + (s1 * r2) by A19, A21, A23, Def4 ;
hence (r1 * s2) + (s1 * r2) = 0. R ; :: thesis: verum

end;

add1 r1,r2,s1,s2,Amp = 0. R by A3, A5, A6, A4, A13, Def16;
then (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = 0. R by VECTSP_1:39
.= (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A14, VECTSP_1:39 ;
hence (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum

end;

case A24: ( 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) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))

A25: gcd r2,s2,Amp divides s2 by Def12;
then A26: gcd r2,s2,Amp divides r1 * s2 by Th7;
then A27: gcd r2,s2,Amp divides (r1 * s2) * r2 by Th7;
then A28: gcd r2,s2,Amp divides ((r1 * s2) * r2) * s2 by Th7;
A29: 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, A6, A4, A24, Def16;
A30: gcd r2,s2,Amp divides r2 by Def12;
then A31: gcd r2,s2,Amp divides s1 * r2 by Th7;
gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides gcd r2,s2,Amp by Def12;
then gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides r2 by A30, Th2;
then A32: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides r2 * (s2 / (gcd r2,s2,Amp)) by Th7;
then A33: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides (r2 * (s2 / (gcd r2,s2,Amp))) * ((r1 * s2) + (s1 * r2)) by Th7;
A34: gcd r2,s2,Amp divides (s1 * r2) * r2 by A30, Th7;
then A35: gcd r2,s2,Amp divides ((s1 * r2) * r2) * s2 by Th7;
A36: gcd r2,s2,Amp divides r2 * s2 by A30, Th7;
then A37: gcd r2,s2,Amp divides (r2 * s2) * r1 by Th7;
then A38: gcd r2,s2,Amp divides ((r2 * s2) * r1) * s2 by Th7;
A39: gcd r2,s2,Amp divides (r2 * s2) * s1 by A36, Th7;
then A40: gcd r2,s2,Amp divides ((r2 * s2) * s1) * r2 by Th7;
A41: 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, A6, A4, A24, Def17;
A42: gcd r2,s2,Amp <> 0. R by A7, Th34;
then A43: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp <> 0. R by Th34;
A44: (r2 * (s2 / (gcd r2,s2,Amp))) * ((r1 * s2) + (s1 * r2)) = ((r2 * (s2 / (gcd r2,s2,Amp))) * (r1 * s2)) + ((r2 * (s2 / (gcd r2,s2,Amp))) * (s1 * r2)) by VECTSP_1:def 11
.= (((r2 * (s2 / (gcd r2,s2,Amp))) * r1) * s2) + ((r2 * (s2 / (gcd r2,s2,Amp))) * (s1 * r2)) by GROUP_1:def 4
.= (((r2 * (s2 / (gcd r2,s2,Amp))) * r1) * s2) + (((r2 * (s2 / (gcd r2,s2,Amp))) * s1) * r2) by GROUP_1:def 4
.= ((((r2 * s2) / (gcd r2,s2,Amp)) * r1) * s2) + (((r2 * (s2 / (gcd r2,s2,Amp))) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) / (gcd r2,s2,Amp)) * r1) * s2) + ((((r2 * s2) / (gcd r2,s2,Amp)) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) * r1) / (gcd r2,s2,Amp)) * s2) + ((((r2 * s2) / (gcd r2,s2,Amp)) * s1) * r2) by A42, A36, A37, Th11
.= ((((r2 * s2) * r1) / (gcd r2,s2,Amp)) * s2) + ((((r2 * s2) * s1) / (gcd r2,s2,Amp)) * r2) by A42, A36, A39, Th11
.= ((((r2 * s2) * r1) * s2) / (gcd r2,s2,Amp)) + ((((r2 * s2) * s1) / (gcd r2,s2,Amp)) * r2) by A42, A37, A38, Th11
.= (((r1 * (s2 * r2)) * s2) / (gcd r2,s2,Amp)) + ((((r2 * s2) * s1) * r2) / (gcd r2,s2,Amp)) by A42, A39, A40, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((((r2 * s2) * s1) * r2) / (gcd r2,s2,Amp)) by GROUP_1:def 4
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((s1 * ((r2 * s2) * r2)) / (gcd r2,s2,Amp)) by GROUP_1:def 4
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((s1 * ((r2 * r2) * s2)) / (gcd r2,s2,Amp)) by GROUP_1:def 4
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + (((s1 * (r2 * r2)) * s2) / (gcd r2,s2,Amp)) by GROUP_1:def 4
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((((s1 * r2) * r2) * s2) / (gcd r2,s2,Amp)) by GROUP_1:def 4 ;
A45: ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) * (r2 * s2) = ((r1 * (s2 / (gcd r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2 / (gcd r2,s2,Amp))) * (r2 * s2)) by VECTSP_1:def 18
.= (((r1 * s2) / (gcd r2,s2,Amp)) * (r2 * s2)) + ((s1 * (r2 / (gcd r2,s2,Amp))) * (r2 * s2)) by A42, A25, A26, Th11
.= (((r1 * s2) / (gcd r2,s2,Amp)) * (r2 * s2)) + (((s1 * r2) / (gcd r2,s2,Amp)) * (r2 * s2)) by A42, A30, A31, Th11
.= ((((r1 * s2) / (gcd r2,s2,Amp)) * r2) * s2) + (((s1 * r2) / (gcd r2,s2,Amp)) * (r2 * s2)) by GROUP_1:def 4
.= ((((r1 * s2) / (gcd r2,s2,Amp)) * r2) * s2) + ((((s1 * r2) / (gcd r2,s2,Amp)) * r2) * s2) by GROUP_1:def 4
.= ((((r1 * s2) * r2) / (gcd r2,s2,Amp)) * s2) + ((((s1 * r2) / (gcd r2,s2,Amp)) * r2) * s2) by A42, A26, A27, Th11
.= ((((r1 * s2) * r2) / (gcd r2,s2,Amp)) * s2) + ((((s1 * r2) * r2) / (gcd r2,s2,Amp)) * s2) by A42, A31, A34, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((((s1 * r2) * r2) / (gcd r2,s2,Amp)) * s2) by A42, A27, A28, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd r2,s2,Amp)) + ((((s1 * r2) * r2) * s2) / (gcd r2,s2,Amp)) by A42, A34, A35, Th11 ;
A46: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) by Def12;
then gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp divides ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) * (r2 * s2) by Th7;
then (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) * (r2 * s2)) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) by A29, A43, A46, Th11
.= (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A41, A45, A44, A43, A32, A33, Th11 ;
hence (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum

end;

end;

end;

hence (add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) ; :: thesis: verum