let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a being Element of R holds
( gcd (a,(1. R),Amp) = 1. R & gcd ((1. R),a,Amp) = 1. R )
let Amp be AmpleSet of R; :: thesis: for a being Element of R holds
( gcd (a,(1. R),Amp) = 1. R & gcd ((1. R),a,Amp) = 1. R )
let A be Element of R; :: thesis: ( gcd (A,(1. R),Amp) = 1. R & gcd ((1. R),A,Amp) = 1. R )
(1. R) * A = A ;
then A1: 1. R divides A ;
( 1. R in Amp & ( for z being Element of R st z divides A & z divides 1. R holds
z divides 1. R ) ) by Def8;
then gcd (A,(1. R),Amp) = 1. R by A1, Def12;
hence ( gcd (A,(1. R),Amp) = 1. R & gcd ((1. R),A,Amp) = 1. R ) by Th29; :: thesis: verum