let n, m, k be Element of NAT ; :: thesis: ( PFArt n,m c= PFArt k,m implies n = k )
assume A1: PFArt n,m c= PFArt k,m ; :: thesis: n = k
assume n <> k ; :: thesis: contradiction
then A2: 2 * n <> 2 * k ;
A3: [(2 * n),m] in PFArt n,m by Def2;
[(2 * n),m] <> [(2 * k),m] by A2, ZFMISC_1:33;
then consider m' being odd Element of NAT such that
A4: ( m' <= 2 * k & [m',m] = [(2 * n),m] ) by A1, A3, Def2;
thus contradiction by A4, ZFMISC_1:33; :: thesis: verum