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: ( A = 0. R & B = 0. R implies gcd A,B,Amp = 0. R )

proof

assume A2: ( A = 0. R & B = 0. R ) ; :: thesis: gcd A,B,Amp = 0. R
then gcd A,B,Amp = NF A,Amp by Th31;
hence gcd A,B,Amp = 0. R by A2, Th25; :: thesis: verum

end;

now

assume gcd A,B,Amp = 0. R ; :: thesis: ( gcd A,B,Amp = 0. R implies ( A = 0. R & B = 0. R ) )
then A3: ( 0. R divides A & 0. R divides B ) by Def12;
then consider D being Element of R such that
A4: (0. R) * D = A by Def1;
consider E being Element of R such that
A5: (0. R) * E = B by A3, Def1;
thus ( gcd A,B,Amp = 0. R implies ( A = 0. R & B = 0. R ) ) by A4, A5, VECTSP_1:39; :: thesis: verum

end;

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