let R be gcdDomain; :: thesis:
let Amp be AmpleSet of R; :: thesis:
let r1, r2, s1, s2 be Element of R; :: thesis:
assume A1: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp ) ; :: thesis:
then ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & s2 in Amp & r2 in Amp ) by Def15;
then A2: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 <> 0. R & s2 <> 0. R & r2 = NF r2,Amp & s2 = NF s2,Amp ) by A1, Def9, Def14, Def15;
then A3: ( gcd r1,s2,Amp <> 0. R & gcd s1,r2,Amp <> 0. R ) by Th34;

now

per cases ;

case A4: ( r1 = 0. R or s1 = 0. R ) ; :: thesis:

then A5: mult1 r1,r2,s1,s2,Amp = 0. R by Def18;

now

per cases by A4;

case r1 = 0. R ; :: thesis:

then (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) = (mult2 r1,r2,s1,s2,Amp) * (0. R) by VECTSP_1:39
.= 0. R by VECTSP_1:39 ;
hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) by A5, VECTSP_1:39; :: thesis:

end;

case s1 = 0. R ; :: thesis:

end;

hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) ; :: thesis:

end;

case A6: ( r2 = 1. R & s2 = 1. R ) ; :: thesis:

then A7: mult1 r1,r2,s1,s2,Amp = r1 * s1 by Def18;
mult2 r1,r2,s1,s2,Amp = 1. R by A2, A6, Def19;
hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) by A6, A7, VECTSP_1:def 13; :: thesis:

end;

case A8: ( s2 <> 0. R & r2 = 1. R ) ; :: thesis:

then A9: mult2 r1,r2,s1,s2,Amp = s2 / (gcd r1,s2,Amp) by A2, Def19;
gcd r1,s2,Amp divides r1 by Def12;
then A10: gcd r1,s2,Amp divides r1 * s1 by Th7;
then A11: gcd r1,s2,Amp divides (r1 * s1) * s2 by Th7;
A12: ((r1 * s1) / (gcd r1,s2,Amp)) * (r2 * s2) = ((r1 * s1) / (gcd r1,s2,Amp)) * s2 by A8, VECTSP_1:def 19
.= ((r1 * s1) * s2) / (gcd r1,s2,Amp) by A3, A10, A11, Th11 ;
A13: gcd r1,s2,Amp divides s2 by Def12;
then A14: gcd r1,s2,Amp divides s2 * r1 by Th7;
then A15: gcd r1,s2,Amp divides (s2 * r1) * s1 by Th7;
(s2 / (gcd r1,s2,Amp)) * (r1 * s1) = ((s2 / (gcd r1,s2,Amp)) * r1) * s1 by GROUP_1:def 4
.= ((s2 * r1) / (gcd r1,s2,Amp)) * s1 by A3, A13, A14, Th11
.= ((s2 * r1) * s1) / (gcd r1,s2,Amp) by A3, A14, A15, Th11
.= ((r1 * s1) * s2) / (gcd r1,s2,Amp) by GROUP_1:def 4 ;
hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) by A8, A9, A12, Def18; :: thesis:

end;

case A16: ( r2 <> 0. R & s2 = 1. R ) ; :: thesis:

then A17: mult2 r1,r2,s1,s2,Amp = r2 / (gcd s1,r2,Amp) by A2, Def19;
gcd s1,r2,Amp divides s1 by Def12;
then A18: gcd s1,r2,Amp divides s1 * r1 by Th7;
then A19: gcd s1,r2,Amp divides (s1 * r1) * r2 by Th7;
A20: ((r1 * s1) / (gcd s1,r2,Amp)) * (r2 * s2) = ((r1 * s1) / (gcd s1,r2,Amp)) * r2 by A16, VECTSP_1:def 13
.= ((r1 * s1) * r2) / (gcd s1,r2,Amp) by A3, A18, A19, Th11 ;
A21: gcd s1,r2,Amp divides r2 by Def12;
then A22: gcd s1,r2,Amp divides r2 * r1 by Th7;
then A23: gcd s1,r2,Amp divides (r2 * r1) * s1 by Th7;
(r2 / (gcd s1,r2,Amp)) * (r1 * s1) = ((r2 / (gcd s1,r2,Amp)) * r1) * s1 by GROUP_1:def 4
.= ((r2 * r1) / (gcd s1,r2,Amp)) * s1 by A3, A21, A22, Th11
.= ((r2 * r1) * s1) / (gcd s1,r2,Amp) by A3, A22, A23, Th11
.= ((r1 * s1) * r2) / (gcd s1,r2,Amp) by GROUP_1:def 4 ;
hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) by A16, A17, A20, Def18; :: thesis:

end;

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

then A25: mult2 r1,r2,s1,s2,Amp = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) by A2, Def19;
A26: gcd r1,s2,Amp divides r1 by Def12;
A27: gcd s1,r2,Amp divides s1 by Def12;
then A28: (gcd r1,s2,Amp) * (gcd s1,r2,Amp) divides r1 * s1 by A26, Th3;
then A29: (gcd r1,s2,Amp) * (gcd s1,r2,Amp) divides (r1 * s1) * r2 by Th7;
then A30: (gcd r1,s2,Amp) * (gcd s1,r2,Amp) divides ((r1 * s1) * r2) * s2 by Th7;
A31: (gcd r1,s2,Amp) * (gcd s1,r2,Amp) <> 0. R by A3, VECTSP_2:def 5;
A32: ((r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp))) * (r2 * s2) = ((r1 * s1) / ((gcd r1,s2,Amp) * (gcd s1,r2,Amp))) * (r2 * s2) by A3, A26, A27, Th14
.= (((r1 * s1) / ((gcd r1,s2,Amp) * (gcd s1,r2,Amp))) * r2) * s2 by GROUP_1:def 4
.= (((r1 * s1) * r2) / ((gcd r1,s2,Amp) * (gcd s1,r2,Amp))) * s2 by A28, A29, A31, Th11
.= (((r1 * s1) * r2) * s2) / ((gcd r1,s2,Amp) * (gcd s1,r2,Amp)) by A29, A30, A31, Th11 ;
A33: gcd s1,r2,Amp divides r2 by Def12;
A34: gcd r1,s2,Amp divides s2 by Def12;
then A35: (gcd s1,r2,Amp) * (gcd r1,s2,Amp) divides r2 * s2 by A33, Th3;
then A36: (gcd s1,r2,Amp) * (gcd r1,s2,Amp) divides (r2 * s2) * r1 by Th7;
then A37: (gcd s1,r2,Amp) * (gcd r1,s2,Amp) divides ((r2 * s2) * r1) * s1 by Th7;
((r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp))) * (r1 * s1) = ((r2 * s2) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp))) * (r1 * s1) by A3, A33, A34, Th14
.= (((r2 * s2) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp))) * r1) * s1 by GROUP_1:def 4
.= (((r2 * s2) * r1) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp))) * s1 by A31, A35, A36, Th11
.= (((r2 * s2) * r1) * s1) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp)) by A31, A36, A37, Th11
.= (r1 * ((r2 * s2) * s1)) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp)) by GROUP_1:def 4
.= (r1 * ((s1 * r2) * s2)) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp)) by GROUP_1:def 4
.= ((r1 * (s1 * r2)) * s2) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp)) by GROUP_1:def 4
.= (((r1 * s1) * r2) * s2) / ((gcd s1,r2,Amp) * (gcd r1,s2,Amp)) by GROUP_1:def 4 ;
hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) by A24, A25, A32, Def18; :: thesis:

end;

hence (mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1) ; :: thesis: