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