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 )
A1: 1. R in Amp by Def8;
(1. R) * A = A by VECTSP_1:def 19;
then A2: 1. R divides A by Def1;
for z being Element of R st z divides A & z divides 1. R holds
z divides 1. R ;
then gcd A,(1. R),Amp = 1. R by A1, A2, Def12;
hence ( gcd A,(1. R),Amp = 1. R & gcd (1. R),A,Amp = 1. R ) by Th30; :: thesis: verum