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:6;
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