let R be gcdDomain; :: thesis: for Amp, Amp' being AmpleSet of R
for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp'
let Amp, Amp' be AmpleSet of R; :: thesis: for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp'
let x, y be Element of R; :: thesis: ( x,y are_canonical_wrt Amp implies x,y are_canonical_wrt Amp' )
assume x,y are_canonical_wrt Amp ; :: thesis: x,y are_canonical_wrt Amp'
then gcd x,y,Amp = 1. R by Def13;
then A1: for z being Element of R st z divides x & z divides y holds
z divides 1. R by Def12;
A2: (1. R) * x = x by VECTSP_1:def 19;
A3: (1. R) * y = y by VECTSP_1:def 19;
A4: 1. R divides x by A2, Def1;
A5: 1. R divides y by A3, Def1;
1. R in Amp' by Def8;
then gcd x,y,Amp' = 1. R by A1, A4, A5, Def12;
hence x,y are_canonical_wrt Amp' by Def13; :: thesis: verum