let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b being Element of R holds
( gcd a,b,Amp = 0. R iff ( a = 0. R & b = 0. R ) )
let Amp be AmpleSet of R; :: thesis: for a, b being Element of R holds
( gcd a,b,Amp = 0. R iff ( a = 0. R & b = 0. R ) )
let A, B be Element of R; :: thesis: ( gcd A,B,Amp = 0. R iff ( A = 0. R & B = 0. R ) )

A1: now

assume A2: gcd A,B,Amp = 0. R ; :: thesis: ( gcd A,B,Amp = 0. R implies ( A = 0. R & B = 0. R ) )
then 0. R divides B by Def12;
then A3: ex E being Element of R st (0. R) * E = B by Def1;
0. R divides A by A2, Def12;
then ex D being Element of R st (0. R) * D = A by Def1;
hence ( gcd A,B,Amp = 0. R implies ( A = 0. R & B = 0. R ) ) by A3, VECTSP_1:39; :: thesis: verum

end;

( A = 0. R & B = 0. R implies gcd A,B,Amp = 0. R )

proof

assume that
A4: A = 0. R and
A5: B = 0. R ; :: thesis: gcd A,B,Amp = 0. R
gcd A,B,Amp = NF A,Amp by A5, Th31;
hence gcd A,B,Amp = 0. R by A4, Th25; :: thesis: verum

end;

hence ( gcd A,B,Amp = 0. R iff ( A = 0. R & B = 0. R ) ) by A1; :: thesis: verum