let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a being Element of R holds
( gcd a,(0. R),Amp = NF a,Amp & gcd (0. R),a,Amp = NF a,Amp )
let Amp be AmpleSet of R; :: thesis: for a being Element of R holds
( gcd a,(0. R),Amp = NF a,Amp & gcd (0. R),a,Amp = NF a,Amp )
let A be Element of R; :: thesis: ( gcd A,(0. R),Amp = NF A,Amp & gcd (0. R),A,Amp = NF A,Amp )
A1: NF A,Amp in Amp by Def9;
(NF A,Amp) * (0. R) = 0. R by VECTSP_1:36;
then A2: NF A,Amp divides 0. R by Def1;
A3: NF A,Amp is_associated_to A by Def9;
A4: for z being Element of R st z divides A & z divides 0. R holds
z divides NF A,Amp

proof

let z be Element of R; :: thesis: ( z divides A & z divides 0. R implies z divides NF A,Amp )
assume that
A5: z divides A and
z divides 0. R ; :: thesis: z divides NF A,Amp
A divides NF A,Amp by A3, Def3;
hence z divides NF A,Amp by A5, Th2; :: thesis: verum

end;

NF A,Amp divides A by A3, Def3;
then gcd A,(0. R),Amp = NF A,Amp by A2, A4, A1, Def12;
hence ( gcd A,(0. R),Amp = NF A,Amp & gcd (0. R),A,Amp = NF A,Amp ) by Th30; :: thesis: verum