let R be gcdDomain; :: thesis: for Amp, Amp9 being AmpleSet of R
for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9
let Amp, Amp9 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 Amp9
let x, y be Element of R; :: thesis: ( x,y are_canonical_wrt Amp implies x,y are_canonical_wrt Amp9 )
(1. R) * x = x by VECTSP_1:def 8;
then A1: 1. R divides x by Def1;
(1. R) * y = y by VECTSP_1:def 8;
then A2: 1. R divides y by Def1;
assume x,y are_canonical_wrt Amp ; :: thesis: x,y are_canonical_wrt Amp9
then gcd (x,y,Amp) = 1. R by Def13;
then A3: for z being Element of R st z divides x & z divides y holds
z divides 1. R by Def12;
1. R in Amp9 by Def8;
then gcd (x,y,Amp9) = 1. R by A3, A1, A2, Def12;
hence x,y are_canonical_wrt Amp9 by Def13; :: thesis: verum